Cyclic Agree and Differential P Indexing [BR09]

[BR09] derive agreement displacement — where the agreement controller alternates between the EA and IA based on person — from cyclic Agree with articulated φ-probes.

This study file connects the Cyclic Agree theory (Syntax/Minimalism/CyclicAgree.lean) to the empirical fragment data for Basque and Georgian, proving that the differential P indexing pattern in both languages is predicted by the partial probe's direct/inverse classification.

Key Result

The central theorem (basque_indexed_iff_always_inverse, georgian_indexed_iff_always_inverse) proves:

An object (IA) is indexed on the verb iff the partial probe puts every EA→IA combination into an inverse context.

SAP objects satisfy this because SAP IAs fully check the partial probe [uπ, uParticipant], leaving no residue for any EA. 3P objects fail it because a SAP EA can match the residue [uParticipant], creating a direct context where the EA — not the object — controls agreement.

Georgian Second-Cycle Morphology

Georgian's m-/v- prefix split for 1sg objects is predicted by the second-cycle information: m- appears when valued on cycle I (IA=1P), v- when valued on cycle II (EA=1P, IA=3P). This connects Georgian objectPrefix to cycleSegments.

def BejarRezac2009.toLevel (c : Agreement.Cell) : Person

Person level of a φ-cell (Agreement.Cell). Basque and Georgian share the same person→level map.

Equations

• BejarRezac2009.toLevel c = match c.person with | some UD.Person.first => Person.first | some UD.Person.second => Person.second | x => Person.third

theorem BejarRezac2009.basque_indexed_eq_sap (c : Agreement.Cell) : c ∈ Agreement.Cell.pnCells → Basque.Agreement.pIsIndexed c = decide (toLevel c).IsSAP

Basque pIsIndexed agrees with Person.isSAP under the bridge.

theorem BejarRezac2009.basque_p1sg_indexed : Basque.Agreement.pIsIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.first Person.first = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.second Person.first = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.third Person.first = true

Per-cell verification: each Basque φ-cell's indexing status matches the cyclic agree prediction.

theorem BejarRezac2009.basque_p2sg_indexed : Basque.Agreement.pIsIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.first Person.second = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.second Person.second = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.third Person.second = true

theorem BejarRezac2009.basque_p3sg_not_indexed : Basque.Agreement.pIsIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = false ∧ Minimalist.CyclicAgree.basque.isInverse Person.first Person.third = false ∧ Minimalist.CyclicAgree.basque.isInverse Person.second Person.third = false

theorem BejarRezac2009.basque_indexed_iff_always_inverse (c : Agreement.Cell) : c ∈ Agreement.Cell.pnCells → (Basque.Agreement.pIsIndexed c = true ↔ ∀ (ea : Person), Minimalist.CyclicAgree.basque.isInverse ea (toLevel c) = true)

Core bridge theorem (Basque): an object is indexed iff cyclic agree puts every EA→IA combination into an inverse context.

When the object (IA) is SAP, the partial probe [uπ, uParticipant] is fully checked by the IA on cycle I, leaving no residue for any EA. Result: IA always controls → agreement tracks the object → indexed.

When the object is 3P, the IA only checks [uπ], leaving [uParticipant] as active residue. A SAP EA matches this residue on cycle II → EA controls → agreement tracks the subject, not the object → not indexed.

theorem BejarRezac2009.georgian_indexed_eq_sap (c : Agreement.Cell) : c ∈ Agreement.Cell.pnCells → Georgian.Agreement.isIndexed c = decide (toLevel c).IsSAP

Georgian isIndexed agrees with Person.isSAP under the bridge.

theorem BejarRezac2009.georgian_1sg_prefix_and_inverse : Georgian.Agreement.objectAgr.realize (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = some "m-" ∧ Minimalist.CyclicAgree.basque.isInverse Person.first Person.first = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.second Person.first = true ∧ Minimalist.CyclicAgree.basque.isInverse Person.third Person.first = true

Per-cell verification: Georgian 1sg object prefix m- exists iff inverse.

theorem BejarRezac2009.georgian_3sg_no_prefix_and_direct : Georgian.Agreement.objectAgr.realize (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = none ∧ Minimalist.CyclicAgree.isDirectContext Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.first Person.third = true ∧ Minimalist.CyclicAgree.isDirectContext Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.second Person.third = true

Per-cell verification: Georgian 3sg has no object prefix, and there exist direct contexts.

theorem BejarRezac2009.georgian_indexed_iff_always_inverse (c : Agreement.Cell) : c ∈ Agreement.Cell.pnCells → (Georgian.Agreement.isIndexed c = true ↔ ∀ (ea : Person), Minimalist.CyclicAgree.basque.isInverse ea (toLevel c) = true)

Core bridge theorem (Georgian): object is indexed iff always inverse.

Georgian uses the same partial probe [u-3-2] and standard geometry as Basque, so the same cyclic agree mechanism derives the same SAP/3P split in object agreement.

theorem BejarRezac2009.georgian_m_is_cycle_I : Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.third Person.first = false ∧ Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.second Person.first = false ∧ Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.first Person.first = false

Georgian 1sg agreement: m- appears when 1P is the IA (cycle I only), v- appears when 1P is the EA (cycle II, IA=3P).

[BR09] §3.2: the m-/v- alternation correlates with whether the probe was valued on the first or second cycle.

theorem BejarRezac2009.georgian_v_is_cycle_II : Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.first Person.third = true ∧ Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.second Person.third = true

theorem BejarRezac2009.georgian_mv_split_is_inverse_direct : (Minimalist.CyclicAgree.basque.isInverse Person.third Person.first = true ∧ Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.third Person.first = false) ∧ Minimalist.CyclicAgree.isDirectContext Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.first Person.third = true ∧ Minimalist.CyclicAgree.hasSecondCycleEffect Minimalist.CyclicAgree.Geometry.standard Minimalist.CyclicAgree.partialProbe Person.first Person.third = true

The m-/v- split is exactly the inverse/direct split for 1P:

• m- (1P object = IA, inverse) → cycle I only, no second-cycle effect
• v- (1P subject = EA, direct) → second-cycle effect present

This connects Georgian objectPrefix morphology to the derivational mechanics of cyclic expansion.

theorem BejarRezac2009.table1_basque_1_2 : Minimalist.CyclicAgree.basque.value Person.first Person.second = Person.second

(2a) 1→2 = 2: "I saw you" — IA controls (inverse).

theorem BejarRezac2009.table1_basque_3_1 : Minimalist.CyclicAgree.basque.value Person.third Person.first = Person.first

(2b) 3→1 = 1: "He saw me" — IA controls (inverse/displacement).

theorem BejarRezac2009.table1_basque_2_1 : Minimalist.CyclicAgree.basque.value Person.second Person.first = Person.first

(2c) 2→1 = 1: "You saw me" — IA controls (inverse/displacement).

theorem BejarRezac2009.table1_basque_1_3 : Minimalist.CyclicAgree.basque.value Person.first Person.third = Person.first

(2d) 1→3 = 1: "I saw him" — EA controls (direct/regular).

theorem BejarRezac2009.table1_basque_2_3 : Minimalist.CyclicAgree.basque.value Person.second Person.third = Person.second

2→3 = 2: "You saw him" — EA controls (direct/regular).

theorem BejarRezac2009.basque_georgian_same_system : Minimalist.CyclicAgree.basque = { geometry := Minimalist.CyclicAgree.Geometry.standard, probe := Minimalist.CyclicAgree.partialProbe } ∧ Minimalist.CyclicAgree.basque = Minimalist.CyclicAgree.basque

Basque and Georgian make the same predictions because they share the same agreement system (standard geometry, partial probe).

theorem BejarRezac2009.cross_linguistic_uniformity : (∀ c ∈ Agreement.Cell.pnCells, Basque.Agreement.pIsIndexed c = decide (toLevel c).IsSAP) ∧ ∀ c ∈ Agreement.Cell.pnCells, Georgian.Agreement.isIndexed c = decide (toLevel c).IsSAP

The differential P indexing pattern is identical for all six person-number φ-cells across both languages.