Documentation

Linglib.Phenomena.Agreement.Studies.BejarRezac2009

Cyclic Agree and Differential P Indexing @cite{bejar-rezac-2009} #

@cite{bejar-rezac-2009} 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 (Theories/Syntax/Minimalism/Core/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 Phenomena.Agreement.Studies.BejarRezac2009.basqueToLevel :

Fragments.Basque.Agreement.PersonNumber → Core.Prominence.PersonLevel

Extract person level from a Basque person-number value.

Equations

Instances For

def Phenomena.Agreement.Studies.BejarRezac2009.georgianToLevel :

Fragments.Georgian.Agreement.PersonNumber → Core.Prominence.PersonLevel

Extract person level from a Georgian person-number value.

Equations

Instances For

theorem Phenomena.Agreement.Studies.BejarRezac2009.basque_indexed_eq_sap (pn : Fragments.Basque.Agreement.PersonNumber) :

Fragments.Basque.Agreement.pIsIndexed pn = (basqueToLevel pn).isSAP

Basque pIsIndexed agrees with PersonLevel.isSAP under the bridge.

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.basque_indexed_iff_always_inverse (pn : Fragments.Basque.Agreement.PersonNumber) :

Fragments.Basque.Agreement.pIsIndexed pn = true ↔ ∀ (ea : Core.Prominence.PersonLevel), Minimalism.CyclicAgree.basque.isInverse ea (basqueToLevel pn) = 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 Phenomena.Agreement.Studies.BejarRezac2009.georgian_indexed_eq_sap (pn : Fragments.Georgian.Agreement.PersonNumber) :

Fragments.Georgian.Agreement.pIsIndexed pn = (georgianToLevel pn).isSAP

Georgian pIsIndexed agrees with PersonLevel.isSAP under the bridge.

theorem Phenomena.Agreement.Studies.BejarRezac2009.georgian_indexed_iff_always_inverse (pn : Fragments.Georgian.Agreement.PersonNumber) :

Fragments.Georgian.Agreement.pIsIndexed pn = true ↔ ∀ (ea : Core.Prominence.PersonLevel), Minimalism.CyclicAgree.basque.isInverse ea (georgianToLevel pn) = 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.

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

@cite{bejar-rezac-2009} §3.2: the m-/v- alternation correlates with whether the probe was valued on the first or second cycle.

theorem Phenomena.Agreement.Studies.BejarRezac2009.georgian_v_is_cycle_II :

Minimalism.CyclicAgree.hasSecondCycleEffect Minimalism.CyclicAgree.Geometry.standard Minimalism.CyclicAgree.partialProbe Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true ∧ Minimalism.CyclicAgree.hasSecondCycleEffect Minimalism.CyclicAgree.Geometry.standard Minimalism.CyclicAgree.partialProbe Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

theorem Phenomena.Agreement.Studies.BejarRezac2009.georgian_mv_split_is_inverse_direct :

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 Phenomena.Agreement.Studies.BejarRezac2009.table1_basque_1_2 :

Minimalism.CyclicAgree.basque.value Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = Core.Prominence.PersonLevel.second

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.table1_basque_3_1 :

Minimalism.CyclicAgree.basque.value Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = Core.Prominence.PersonLevel.first

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.table1_basque_2_1 :

Minimalism.CyclicAgree.basque.value Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = Core.Prominence.PersonLevel.first

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.table1_basque_1_3 :

Minimalism.CyclicAgree.basque.value Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.first

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.table1_basque_2_3 :

Minimalism.CyclicAgree.basque.value Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = Core.Prominence.PersonLevel.second

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.basque_georgian_same_system :

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

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

theorem Phenomena.Agreement.Studies.BejarRezac2009.cross_linguistic_uniformity :

(∀ (pn : Fragments.Basque.Agreement.PersonNumber), Fragments.Basque.Agreement.pIsIndexed pn = (basqueToLevel pn).isSAP) ∧ ∀ (pn : Fragments.Georgian.Agreement.PersonNumber), Fragments.Georgian.Agreement.pIsIndexed pn = (georgianToLevel pn).isSAP

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