Cyclic Agree @cite{bejar-rezac-2009}

@cite{bejar-rezac-2009} derive person hierarchy (PH) effects from three independently motivated mechanisms:

1. Articulated φ-features: person is decomposed into hierarchical segments — [π] ⊂ [participant] ⊂ [speaker]/[addressee] — each of which can independently enter Agree.
2. Feature-relativized locality: a probe segment [uF] only sees goals bearing [F]; a goal lacking [F] is bypassed, leaving an active residue.
3. Cyclic expansion: v's probe first Agrees with the IA (cycle I), then with the EA (cycle II). The IA is preferred because cyclicity puts it in the search space first.

The interaction of probe articulation and cyclic Agree derives:

• Agreement displacement: IA agreement bleeds EA agreement when the IA fully checks the probe. When it doesn't, residue reaches the EA.
• Direct/Inverse contexts: Inverse = core probe doesn't Agree with EA (IA fully checks, or EA can't match the residue). Direct = EA Agrees with residue segments.
• Crosslinguistic variation: languages differ in probe articulation — flat [u-3] (no PH sensitivity), partial [u-3-2] (SAP vs 3P), or full [u-3-2-1] (all persons distinguished).

Person Geometries

Two attested geometries for the innermost feature:

• Standard (1>2>3): [speaker] distinguishes 1st from 2nd. Used by Basque, Georgian (@cite{bejar-rezac-2009} Table 2B).
• Addressee (2>1>3): [addressee] distinguishes 2nd from 1st. Used by Nishnaabemwin, Mohawk (@cite{bejar-rezac-2009} Table 2C).

Person Licensing and Repair

The Person-Licensing Condition (PLC) requires every π-feature to be licensed by Agree. In inverse contexts, the EA's π-features are not licensed by the core probe, triggering repair strategies:

• Added probe: an extra probe is inserted on v_II in inverse contexts (Nishnaabemwin, Mohawk, Basque)
• R-Case: the IA receives a special oblique Case (Kashmiri)

Both strategies are derivationally bounded: they occur in all and only inverse contexts.

Integration

Connects to PersonGeometry.lean via bridge theorems. The direct/inverse classification predicts which languages show differential P indexing (Basque, Georgian fragments).

inductive Minimalism.CyclicAgree.Segment : Type

A single segment in an articulated person feature structure.

Segments are privative features organized in a containment hierarchy. Every person value bears [π]; SAPs additionally bear [participant]; the innermost feature ([speaker] or [addressee]) distinguishes 1st from 2nd person.

• pi : Segment
• participant : Segment
• speaker : Segment
• addressee : Segment

instance Minimalism.CyclicAgree.instDecidableEqSegment : DecidableEq Segment

Equations

• Minimalism.CyclicAgree.instDecidableEqSegment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.CyclicAgree.instBEqSegment : BEq Segment

Equations

• Minimalism.CyclicAgree.instBEqSegment = { beq := Minimalism.CyclicAgree.instBEqSegment.beq }

def Minimalism.CyclicAgree.instBEqSegment.beq : Segment → Segment → Bool

Equations

• Minimalism.CyclicAgree.instBEqSegment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Minimalism.CyclicAgree.instReprSegment.repr : Segment → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Minimalism.CyclicAgree.instReprSegment : Repr Segment

Equations

• Minimalism.CyclicAgree.instReprSegment = { reprPrec := Minimalism.CyclicAgree.instReprSegment.repr }

instance Minimalism.CyclicAgree.instInhabitedSegment : Inhabited Segment

Equations

• Minimalism.CyclicAgree.instInhabitedSegment = { default := Minimalism.CyclicAgree.instInhabitedSegment.default }

def Minimalism.CyclicAgree.instInhabitedSegment.default : Segment

Equations

• Minimalism.CyclicAgree.instInhabitedSegment.default = Minimalism.CyclicAgree.Segment.pi

inductive Minimalism.CyclicAgree.Geometry : Type

Which feature distinguishes 1st from 2nd person.

• standard: [speaker] distinguishes 1st (Basque, Georgian)
• addressee: [addressee] distinguishes 2nd (Nishnaabemwin, Mohawk)

• standard : Geometry
• addressee : Geometry

instance Minimalism.CyclicAgree.instDecidableEqGeometry : DecidableEq Geometry

Equations

• Minimalism.CyclicAgree.instDecidableEqGeometry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.CyclicAgree.instBEqGeometry.beq : Geometry → Geometry → Bool

Equations

• Minimalism.CyclicAgree.instBEqGeometry.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.CyclicAgree.instBEqGeometry : BEq Geometry

Equations

• Minimalism.CyclicAgree.instBEqGeometry = { beq := Minimalism.CyclicAgree.instBEqGeometry.beq }

instance Minimalism.CyclicAgree.instReprGeometry : Repr Geometry

Equations

• Minimalism.CyclicAgree.instReprGeometry = { reprPrec := Minimalism.CyclicAgree.instReprGeometry.repr }

def Minimalism.CyclicAgree.instReprGeometry.repr : Geometry → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.personSpec (geom : Geometry) : Core.Prominence.PersonLevel → List Segment

The person specification for a given person value under a geometry.

Returns the list of segments a DP of this person bears.

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.CyclicAgree.personSpec geom Core.Prominence.PersonLevel.third = [Minimalism.CyclicAgree.Segment.pi]
• Minimalism.CyclicAgree.personSpec Minimalism.CyclicAgree.Geometry.addressee Core.Prominence.PersonLevel.first = [Minimalism.CyclicAgree.Segment.pi, Minimalism.CyclicAgree.Segment.participant]
• Minimalism.CyclicAgree.personSpec Minimalism.CyclicAgree.Geometry.standard Core.Prominence.PersonLevel.second = [Minimalism.CyclicAgree.Segment.pi, Minimalism.CyclicAgree.Segment.participant]

def Minimalism.CyclicAgree.mostSpecified : Geometry → Core.Prominence.PersonLevel

The most specified person under a given geometry.

Equations

• Minimalism.CyclicAgree.mostSpecified Minimalism.CyclicAgree.Geometry.standard = Core.Prominence.PersonLevel.first
• Minimalism.CyclicAgree.mostSpecified Minimalism.CyclicAgree.Geometry.addressee = Core.Prominence.PersonLevel.second

@[reducible, inline]

abbrev Minimalism.CyclicAgree.ProbeArticulation : Type

An articulated probe: a list of unvalued segments, ordered from outermost (most general) to innermost (most specific).

Languages vary parametrically in probe articulation:

• Flat [u-3]: no PH sensitivity (e.g., Swahili, Abkhaz)
• Partial [u-3-2]: distinguishes SAP from 3P (e.g., Basque, Georgian)
• Full [u-3-2-1]: distinguishes all persons (e.g., Nishnaabemwin, Mohawk)

Equations

• Minimalism.CyclicAgree.ProbeArticulation = List Minimalism.CyclicAgree.Segment

def Minimalism.CyclicAgree.flatProbe : ProbeArticulation

Flat probe: [uπ]. Any DP fully matches.

Equations

• Minimalism.CyclicAgree.flatProbe = [Minimalism.CyclicAgree.Segment.pi]

def Minimalism.CyclicAgree.partialProbe : ProbeArticulation

Partial probe: [uπ, uParticipant]. Distinguishes SAP from 3P. Geometry-independent: [participant] is the same in both geometries.

Equations

• Minimalism.CyclicAgree.partialProbe = [Minimalism.CyclicAgree.Segment.pi, Minimalism.CyclicAgree.Segment.participant]

def Minimalism.CyclicAgree.fullProbeStd : ProbeArticulation

Full probe in standard geometry: [uπ, uParticipant, uSpeaker].

Equations

• Minimalism.CyclicAgree.fullProbeStd = [Minimalism.CyclicAgree.Segment.pi, Minimalism.CyclicAgree.Segment.participant, Minimalism.CyclicAgree.Segment.speaker]

def Minimalism.CyclicAgree.fullProbeAddr : ProbeArticulation

Full probe in addressee geometry: [uπ, uParticipant, uAddressee].

Equations

• Minimalism.CyclicAgree.fullProbeAddr = [Minimalism.CyclicAgree.Segment.pi, Minimalism.CyclicAgree.Segment.participant, Minimalism.CyclicAgree.Segment.addressee]

structure Minimalism.CyclicAgree.AgreementSystem : Type

A language's agreement system: the geometry and characteristic probe.

@cite{bejar-rezac-2009} parameterize crosslinguistic variation by two choices: (1) which geometry organizes the innermost feature, and (2) how articulated the probe is. The full probe depends on the geometry (standard uses [speaker], addressee uses [addressee]).

• geometry : Geometry
• probe : ProbeArticulation

def Minimalism.CyclicAgree.instDecidableEqAgreementSystem.decEq (x✝ x✝¹ : AgreementSystem) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance Minimalism.CyclicAgree.instDecidableEqAgreementSystem : DecidableEq AgreementSystem

Equations

• Minimalism.CyclicAgree.instDecidableEqAgreementSystem = Minimalism.CyclicAgree.instDecidableEqAgreementSystem.decEq

def Minimalism.CyclicAgree.instBEqAgreementSystem.beq : AgreementSystem → AgreementSystem → Bool

Equations

• Minimalism.CyclicAgree.instBEqAgreementSystem.beq { geometry := a, probe := a_1 } { geometry := b, probe := b_1 } = (a == b && a_1 == b_1)
• Minimalism.CyclicAgree.instBEqAgreementSystem.beq x✝¹ x✝ = false

instance Minimalism.CyclicAgree.instBEqAgreementSystem : BEq AgreementSystem

Equations

• Minimalism.CyclicAgree.instBEqAgreementSystem = { beq := Minimalism.CyclicAgree.instBEqAgreementSystem.beq }

instance Minimalism.CyclicAgree.instReprAgreementSystem : Repr AgreementSystem

Equations

• Minimalism.CyclicAgree.instReprAgreementSystem = { reprPrec := Minimalism.CyclicAgree.instReprAgreementSystem.repr }

def Minimalism.CyclicAgree.instReprAgreementSystem.repr : AgreementSystem → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.swahili : AgreementSystem

Swahili/Abkhaz: flat probe, no PH sensitivity.

Equations

• Minimalism.CyclicAgree.swahili = { geometry := Minimalism.CyclicAgree.Geometry.standard, probe := Minimalism.CyclicAgree.flatProbe }

def Minimalism.CyclicAgree.basque : AgreementSystem

Basque/Georgian: partial probe, standard geometry.

Equations

• Minimalism.CyclicAgree.basque = { geometry := Minimalism.CyclicAgree.Geometry.standard, probe := Minimalism.CyclicAgree.partialProbe }

def Minimalism.CyclicAgree.nishnaabemwin : AgreementSystem

Nishnaabemwin/Mohawk: full probe, addressee geometry.

Equations

• Minimalism.CyclicAgree.nishnaabemwin = { geometry := Minimalism.CyclicAgree.Geometry.addressee, probe := Minimalism.CyclicAgree.fullProbeAddr }

def Minimalism.CyclicAgree.activeResidue (probe : ProbeArticulation) (goal : List Segment) : ProbeArticulation

Active residue: unmatched probe segments after Agree with a goal DP.

Each probe segment that has a corresponding segment in the goal's person specification is deactivated (matched). Segments without a match remain active and can participate in further Agree on the next cycle.

This is the core operation of @cite{bejar-rezac-2009}: partial matching of articulated probes drives agreement displacement.

Equations

• Minimalism.CyclicAgree.activeResidue probe goal = List.filter (fun (s : Minimalism.CyclicAgree.Segment) => !goal.contains s) probe

inductive Minimalism.CyclicAgree.Controller : Type

Which argument controls the core agreement slot.

• ia : Controller
• ea : Controller

instance Minimalism.CyclicAgree.instDecidableEqController : DecidableEq Controller

Equations

• Minimalism.CyclicAgree.instDecidableEqController x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.CyclicAgree.instBEqController : BEq Controller

Equations

• Minimalism.CyclicAgree.instBEqController = { beq := Minimalism.CyclicAgree.instBEqController.beq }

def Minimalism.CyclicAgree.instBEqController.beq : Controller → Controller → Bool

Equations

• Minimalism.CyclicAgree.instBEqController.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.CyclicAgree.instReprController : Repr Controller

Equations

• Minimalism.CyclicAgree.instReprController = { reprPrec := Minimalism.CyclicAgree.instReprController.repr }

def Minimalism.CyclicAgree.instReprController.repr : Controller → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.eaAgrees (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Bool

Does the EA Agree with residue segments on cycle II?

Returns true iff the EA matches at least one segment that the IA left unmatched.

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.agreementController (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Controller

Determine which argument controls the core agreement slot.

Cycle I: probe Agrees with IA. If residue remains, cycle II: probe Agrees with EA. EA controls iff it matches any residue segment; otherwise IA controls (either it fully checked the probe, or it left residue the EA couldn't match).

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.agreementValue (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Core.Prominence.PersonLevel

The person value that the core agreement slot realizes.

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.AgreementSystem.controller (sys : AgreementSystem) (ea ia : Core.Prominence.PersonLevel) : Controller

Convenience: controller using an AgreementSystem.

Equations

• sys.controller ea ia = Minimalism.CyclicAgree.agreementController sys.geometry sys.probe ea ia

def Minimalism.CyclicAgree.AgreementSystem.value (sys : AgreementSystem) (ea ia : Core.Prominence.PersonLevel) : Core.Prominence.PersonLevel

Convenience: agreement value using an AgreementSystem.

Equations

• sys.value ea ia = Minimalism.CyclicAgree.agreementValue sys.geometry sys.probe ea ia

def Minimalism.CyclicAgree.cycleSegments (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : ProbeArticulation × ProbeArticulation

Which cycle valued the probe's remaining segments.

@cite{bejar-rezac-2009} §3.2: when the probe is valued on two different cycles, the morphological realization can differ. Georgian uses m- (first cycle) vs v- (second cycle) for 1sg agreement; Nishnaabemwin uses -in (1P, cycle II) vs -igw (3P, cycle II) vs -aa (default/cycle I only).

Returns (cycleI, cycleII) — the segments deactivated on each cycle.

Equations

• One or more equations did not get rendered due to their size.

def Minimalism.CyclicAgree.hasSecondCycleEffect (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Bool

Was the probe valued on two distinct cycles?

True when both the IA (cycle I) and EA (cycle II) matched at least one segment. This is the configuration that creates second-cycle morphological effects in languages like Georgian and Nishnaabemwin.

Equations

• Minimalism.CyclicAgree.hasSecondCycleEffect geom probe ea ia = match Minimalism.CyclicAgree.cycleSegments geom probe ea ia with | (c1, c2) => !List.isEmpty c1 && !List.isEmpty c2

def Minimalism.CyclicAgree.isInverseContext (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Bool

Inverse context: the core π-probe on v does NOT Agree with the EA.

This occurs when either (a) the IA fully checks the probe, leaving no residue, or (b) residue exists but the EA cannot match any of it. Inverse contexts trigger PLC violations on the EA's π-features, requiring repair strategies (added probe or R-Case).

Equations

• Minimalism.CyclicAgree.isInverseContext geom probe ea ia = !Minimalism.CyclicAgree.eaAgrees geom probe ea ia

def Minimalism.CyclicAgree.isDirectContext (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Bool

Direct context: the EA Agrees with at least one residue segment.

Equations

• Minimalism.CyclicAgree.isDirectContext geom probe ea ia = Minimalism.CyclicAgree.eaAgrees geom probe ea ia

def Minimalism.CyclicAgree.AgreementSystem.isInverse (sys : AgreementSystem) (ea ia : Core.Prominence.PersonLevel) : Bool

Convenience: inverse using an AgreementSystem.

Equations

• sys.isInverse ea ia = Minimalism.CyclicAgree.isInverseContext sys.geometry sys.probe ea ia

def Minimalism.CyclicAgree.eaIsLicensed (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : Bool

The Person-Licensing Condition (PLC).

@cite{bejar-rezac-2009} eq. (13): "A π-feature [F] must be licensed by Agree of some segment in a feature structure of which [F] is a subset."

In inverse contexts, the EA's π-features are not licensed by the core probe (because the probe either has no residue or residue the EA can't match). This drives repair strategies.

Returns true if the EA is person-licensed (its π-features were checked by the core probe on cycle II).

Equations

• Minimalism.CyclicAgree.eaIsLicensed geom probe ea ia = Minimalism.CyclicAgree.eaAgrees geom probe ea ia

theorem Minimalism.CyclicAgree.plc_violation_iff_inverse (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : eaIsLicensed geom probe ea ia = false ↔ isInverseContext geom probe ea ia = true

PLC violation: EA is NOT person-licensed. Exactly characterizes inverse contexts — this is the paper's key insight connecting syntactic derivation to morphological repair.

inductive Minimalism.CyclicAgree.RepairStrategy : Type

Repair strategies for PLC violations in inverse contexts.

@cite{bejar-rezac-2009} §4 identifies two strategies:

• addedProbe: an extra probe is inserted on v_II, creating an additional agreement slot for the EA (Nishnaabemwin, Mohawk, Basque)
• rCase: the IA receives a special oblique Case distinct from the regular v-assigned Case (Kashmiri)

• addedProbe : RepairStrategy
• rCase : RepairStrategy

instance Minimalism.CyclicAgree.instDecidableEqRepairStrategy : DecidableEq RepairStrategy

Equations

• Minimalism.CyclicAgree.instDecidableEqRepairStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.CyclicAgree.instBEqRepairStrategy : BEq RepairStrategy

Equations

• Minimalism.CyclicAgree.instBEqRepairStrategy = { beq := Minimalism.CyclicAgree.instBEqRepairStrategy.beq }

def Minimalism.CyclicAgree.instBEqRepairStrategy.beq : RepairStrategy → RepairStrategy → Bool

Equations

• Minimalism.CyclicAgree.instBEqRepairStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Minimalism.CyclicAgree.instReprRepairStrategy.repr : RepairStrategy → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Minimalism.CyclicAgree.instReprRepairStrategy : Repr RepairStrategy

Equations

• Minimalism.CyclicAgree.instReprRepairStrategy = { reprPrec := Minimalism.CyclicAgree.instReprRepairStrategy.repr }

def Minimalism.CyclicAgree.needsRepair (sys : AgreementSystem) (ea ia : Core.Prominence.PersonLevel) : Bool

Does a given EA→IA combination require repair under this system?

Repair is needed iff the context is inverse.

Equations

• Minimalism.CyclicAgree.needsRepair sys ea ia = sys.isInverse ea ia

theorem Minimalism.CyclicAgree.std_participant_matches_decomposed (p : Core.Prominence.PersonLevel) : (personSpec Geometry.standard p).contains Segment.participant = (decomposePerson p).hasParticipant

In the standard geometry, a person value has [participant] as a segment iff DecomposedPerson.hasParticipant is true.

theorem Minimalism.CyclicAgree.std_third_singleton : personSpec Geometry.standard Core.Prominence.PersonLevel.third = [Segment.pi]

In the standard geometry, 3rd person has exactly one segment ([π]).

theorem Minimalism.CyclicAgree.std_spec_lengths : (personSpec Geometry.standard Core.Prominence.PersonLevel.first).length = 3 ∧ (personSpec Geometry.standard Core.Prominence.PersonLevel.second).length = 2 ∧ (personSpec Geometry.standard Core.Prominence.PersonLevel.third).length = 1

Segment count reflects the person hierarchy: 1st (3 segments) > 2nd (2) > 3rd (1) in standard geometry.

theorem Minimalism.CyclicAgree.std_first_entails_second (s : Segment) : s ∈ personSpec Geometry.standard Core.Prominence.PersonLevel.second → s ∈ personSpec Geometry.standard Core.Prominence.PersonLevel.first

Entailment: more specified persons' segments are supersets.

theorem Minimalism.CyclicAgree.std_second_entails_third (s : Segment) : s ∈ personSpec Geometry.standard Core.Prominence.PersonLevel.third → s ∈ personSpec Geometry.standard Core.Prominence.PersonLevel.second

theorem Minimalism.CyclicAgree.flat_no_residue (geom : Geometry) (ia : Core.Prominence.PersonLevel) : activeResidue flatProbe (personSpec geom ia) = []

Flat probe: IA always fully checks the probe, regardless of person.

theorem Minimalism.CyclicAgree.flat_ia_controls (geom : Geometry) (ea ia : Core.Prominence.PersonLevel) : agreementController geom flatProbe ea ia = Controller.ia

Flat probe: IA always controls — no PH effects.

theorem Minimalism.CyclicAgree.flat_all_inverse (geom : Geometry) (ea ia : Core.Prominence.PersonLevel) : isInverseContext geom flatProbe ea ia = true

Flat probe: all contexts are inverse (no EA agreement).

theorem Minimalism.CyclicAgree.partial_geometry_invariant (ea ia : Core.Prominence.PersonLevel) : agreementValue Geometry.standard partialProbe ea ia = agreementValue Geometry.addressee partialProbe ea ia

Partial probe: same behavior in both geometries, since [participant] is geometry-independent.

theorem Minimalism.CyclicAgree.basque_3_1 : basque.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = Core.Prominence.PersonLevel.first

Basque: 3→1 = 1 (IA controls, inverse).

theorem Minimalism.CyclicAgree.basque_2_1 : basque.value Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = Core.Prominence.PersonLevel.first

Basque: 2→1 = 1 (IA controls, inverse).

theorem Minimalism.CyclicAgree.basque_1_2 : basque.value Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = Core.Prominence.PersonLevel.second

Basque: 1→2 = 2 (IA controls, inverse).

theorem Minimalism.CyclicAgree.basque_3_2 : basque.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = Core.Prominence.PersonLevel.second

Basque: 3→2 = 2 (IA controls, inverse).

theorem Minimalism.CyclicAgree.basque_1_3 : basque.value Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.first

Basque: 1→3 = 1 (EA controls, direct).

theorem Minimalism.CyclicAgree.basque_2_3 : basque.value Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.second

Basque: 2→3 = 2 (EA controls, direct).

theorem Minimalism.CyclicAgree.basque_3_3 : basque.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.third

Basque: 3→3 = 3 (IA controls, inverse — residue [uParticipant] unmatched by either argument).

theorem Minimalism.CyclicAgree.basque_sap_ia_inverse (ea : Core.Prominence.PersonLevel) : basque.isInverse ea Core.Prominence.PersonLevel.first = true ∧ basque.isInverse ea Core.Prominence.PersonLevel.second = true

Basque: SAP IA → inverse context (agreement displacement to IA).

theorem Minimalism.CyclicAgree.basque_3p_ia_direct (ea : Core.Prominence.PersonLevel) (h : ea ≠ Core.Prominence.PersonLevel.third) : isDirectContext Geometry.standard partialProbe ea Core.Prominence.PersonLevel.third = true

Basque: 3P IA + SAP EA → direct context (EA controls).

theorem Minimalism.CyclicAgree.basque_3_3_inverse : basque.isInverse Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

Basque: 3P IA + 3P EA → inverse (neither fully checks).

theorem Minimalism.CyclicAgree.nish_3_2 : nishnaabemwin.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = Core.Prominence.PersonLevel.second

Nishnaabemwin: 3→2 = 2 (IA controls, inverse — IA fully checks).

theorem Minimalism.CyclicAgree.nish_1_2 : nishnaabemwin.value Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = Core.Prominence.PersonLevel.second

Nishnaabemwin: 1→2 = 2 (IA controls, inverse — IA fully checks).

theorem Minimalism.CyclicAgree.nish_3_1 : nishnaabemwin.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = Core.Prominence.PersonLevel.first

Nishnaabemwin: 3→1 = 1 (IA controls, inverse — EA can't match residue).

theorem Minimalism.CyclicAgree.nish_2_1 : nishnaabemwin.value Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = Core.Prominence.PersonLevel.second

Nishnaabemwin: 2→1 = 2 (EA controls, direct — EA matches [uAddressee]).

theorem Minimalism.CyclicAgree.nish_1_3 : nishnaabemwin.value Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.first

Nishnaabemwin: 1→3 = 1 (EA controls, direct).

theorem Minimalism.CyclicAgree.nish_2_3 : nishnaabemwin.value Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.second

Nishnaabemwin: 2→3 = 2 (EA controls, direct).

theorem Minimalism.CyclicAgree.nish_3_3 : nishnaabemwin.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.third

Nishnaabemwin: 3→3 = 3 (IA controls, inverse — residue [uParticipant, uAddressee] unmatched by 3P EA).

theorem Minimalism.CyclicAgree.nish_2p_ia_inverse (ea : Core.Prominence.PersonLevel) : nishnaabemwin.isInverse ea Core.Prominence.PersonLevel.second = true

Nishnaabemwin: 2P IA → always inverse (2nd is most specified).

theorem Minimalism.CyclicAgree.nish_3p_ia_sap_ea_direct : isDirectContext Geometry.addressee fullProbeAddr Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true ∧ isDirectContext Geometry.addressee fullProbeAddr Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

Nishnaabemwin: 3P IA with SAP EA → direct.

theorem Minimalism.CyclicAgree.nish_3_1_inverse : nishnaabemwin.isInverse Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = true

Nishnaabemwin: 3→1 is inverse despite residue, because EA (3P) can't match [addressee].

theorem Minimalism.CyclicAgree.nish_3_3_inverse : nishnaabemwin.isInverse Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

Nishnaabemwin: 3→3 is inverse.

theorem Minimalism.CyclicAgree.georgian_1_3_second_cycle : hasSecondCycleEffect Geometry.standard partialProbe Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

Georgian second-cycle effect: 1sg agreement is m- when valued on cycle I (IA=1, any EA), but v- when valued on cycle II (EA=1, IA=3).

theorem Minimalism.CyclicAgree.georgian_no_second_cycle_sap_ia (ea : Core.Prominence.PersonLevel) : hasSecondCycleEffect Geometry.standard partialProbe ea Core.Prominence.PersonLevel.first = false ∧ hasSecondCycleEffect Geometry.standard partialProbe ea Core.Prominence.PersonLevel.second = false

Georgian: when IA is SAP, no second cycle (IA fully checks).

theorem Minimalism.CyclicAgree.nish_2_1_second_cycle : hasSecondCycleEffect Geometry.addressee fullProbeAddr Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = true

Nishnaabemwin: 2→1 has a second-cycle effect (IA checks [π,participant], EA checks [addressee] on cycle II).

theorem Minimalism.CyclicAgree.nish_2_1_cycle_segments : (cycleSegments Geometry.addressee fullProbeAddr Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first).snd = [Segment.addressee]

Nishnaabemwin: the second cycle in 2→1 values exactly [addressee].

theorem Minimalism.CyclicAgree.same_person_ia_controls (geom : Geometry) (probe : ProbeArticulation) (p : Core.Prominence.PersonLevel) : agreementController geom probe p p = Controller.ia

When EA and IA have the same person, IA always controls (the EA contributes nothing new — every segment it could match was already matched by the identical IA).

The proof proceeds by showing that activeResidue is idempotent when applied with the same goal: if some segments survive matching against personSpec(p), applying the same filter again removes nothing, so eaAgrees returns false.

theorem Minimalism.CyclicAgree.most_specified_controls_vs_third_std : agreementValue Geometry.standard fullProbeStd (mostSpecified Geometry.standard) Core.Prominence.PersonLevel.third = mostSpecified Geometry.standard ∧ agreementValue Geometry.standard fullProbeStd Core.Prominence.PersonLevel.third (mostSpecified Geometry.standard) = mostSpecified Geometry.standard

The most specified person always controls against 3P (standard).

theorem Minimalism.CyclicAgree.most_specified_controls_vs_third_addr : agreementValue Geometry.addressee fullProbeAddr (mostSpecified Geometry.addressee) Core.Prominence.PersonLevel.third = mostSpecified Geometry.addressee ∧ agreementValue Geometry.addressee fullProbeAddr Core.Prominence.PersonLevel.third (mostSpecified Geometry.addressee) = mostSpecified Geometry.addressee

The most specified person always controls against 3P (addressee).

theorem Minimalism.CyclicAgree.direct_inverse_exhaustive (geom : Geometry) (probe : ProbeArticulation) (ea ia : Core.Prominence.PersonLevel) : (isDirectContext geom probe ea ia = true) ≠ (isInverseContext geom probe ea ia = true)

The direct/inverse split exhaustively partitions the paradigm: every EA→IA combination is either direct or inverse, never both.

theorem Minimalism.CyclicAgree.partial_probe_sap_ia_is_inverse (ea : Core.Prominence.PersonLevel) : isInverseContext Geometry.standard partialProbe ea Core.Prominence.PersonLevel.first = true ∧ isInverseContext Geometry.standard partialProbe ea Core.Prominence.PersonLevel.second = true

In a partial-probe language like Basque/Georgian, object (P) agreement is person-conditioned: the object controls agreement iff the context is direct (EA > IA on the person hierarchy). This predicts that SAP objects trigger agreement displacement to EA, while 3P objects don't.

Formally: for a fixed 3P EA (the "subject" in a canonical transitive), a SAP IA triggers direct context (EA controls → "no P indexing"), but this is backwards from the traditional description. Let's think about it from the P indexing perspective:

In Basque, the agreement slot tracks the controller. When IA is SAP, IA controls (inverse) — the agreement tracks IA, reflecting the object. When IA is 3P, EA controls (direct) — agreement tracks EA, not the object.

So pIsIndexed ↔ the IA controls (the agreement slot shows the object's features) ↔ inverse context.

theorem Minimalism.CyclicAgree.partial_probe_3p_ia_sap_ea_is_direct : isDirectContext Geometry.standard partialProbe Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true ∧ isDirectContext Geometry.standard partialProbe Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

3P IA yields direct context when EA is SAP — the agreement slot tracks the EA, not the (3P) object.

theorem Minimalism.CyclicAgree.sap_ia_indexed_via_inverse (p : Core.Prominence.PersonLevel) (h : p ≠ Core.Prominence.PersonLevel.third) (ea : Core.Prominence.PersonLevel) : isInverseContext Geometry.standard partialProbe ea p = true

Differential P indexing prediction: the SAP/3P split in object agreement (Basque pIsIndexed, Georgian pIsIndexed) is exactly the inverse/direct split of the partial probe.

An object (IA) is "indexed" when the core agreement slot tracks the IA's person features, which happens iff the context is inverse (IA controls). SAP IAs always produce inverse contexts; 3P IAs produce direct contexts (when EA is SAP).

This theorem proves the key direction: SAP IA → inverse (indexed).

def Minimalism.CyclicAgree.inverseCount (sys : AgreementSystem) : Nat

Count inverse contexts in a 3×3 paradigm.

Equations

• One or more equations did not get rendered due to their size.

theorem Minimalism.CyclicAgree.swahili_all_inverse : inverseCount swahili = 9

Swahili (flat): all 9 cells are inverse (no PH sensitivity).

theorem Minimalism.CyclicAgree.basque_inverse_count : inverseCount basque = 7

Basque (partial): 7 inverse, 2 direct (only SAP EA + 3P IA).

theorem Minimalism.CyclicAgree.nish_inverse_count : inverseCount nishnaabemwin = 6

Nishnaabemwin (full): 6 inverse, 3 direct.

theorem Minimalism.CyclicAgree.articulation_increases_direct : inverseCount swahili ≥ inverseCount basque ∧ inverseCount basque ≥ inverseCount nishnaabemwin

More articulated probes yield more direct contexts.