Cyclic Agree [BR09]

[BR09] 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 ([BR09] Table 2B).
• Addressee (2>1>3): [addressee] distinguishes 2nd from 1st. Used by Nishnaabemwin, Mohawk ([BR09] 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 Phi/Geometry.lean via bridge theorems. The direct/inverse classification predicts which languages show differential P indexing (Basque, Georgian fragments).

Sibling mechanisms in Syntax/Minimalism/

NestedAgree.lean ([Ama25]) and Long-Distance Agree ([Sza09], Studies/Allotey2021.lean) are sibling Layer-2 patterns. All three address what a probe does beyond its first operation, but differently:

• Cyclic Agree (this file): single articulated probe with multiple feature segments; cycle II's residue probing expands the domain to reach the EA after the IA partially checks the probe.
• Nested Agree: multiple ordered probes on one head, all forced under maximized matching to target the same goal; each subsequent probe operates on a truncated domain restricted to the first goal's daughters.
• Long-Distance Agree: a single probe relaxes clause-locality across a non-defective C.

The three are conceptually orthogonal — Cyclic addresses articulation, Nested addresses ordering, LDA addresses clause-boundedness. A given construction may instantiate one but not the others.

inductive Minimalist.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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instDecidableEqSegment : DecidableEq Segment

Equations

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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instReprSegment : Repr Segment

Equations

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

def Minimalist.CyclicAgree.instReprSegment.repr : Segment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instInhabitedSegment : Inhabited Segment

Equations

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

inductive Minimalist.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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instDecidableEqGeometry : DecidableEq Geometry

Equations

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

def Minimalist.CyclicAgree.instReprGeometry.repr : Geometry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instReprGeometry : Repr Geometry

Equations

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

def Minimalist.CyclicAgree.personSpec (geom : Geometry) : Person → 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.
• Minimalist.CyclicAgree.personSpec geom Person.third = [Minimalist.CyclicAgree.Segment.pi]
• Minimalist.CyclicAgree.personSpec geom Person.zero = [Minimalist.CyclicAgree.Segment.pi]
• Minimalist.CyclicAgree.personSpec Minimalist.CyclicAgree.Geometry.addressee Person.first = [Minimalist.CyclicAgree.Segment.pi, Minimalist.CyclicAgree.Segment.participant]
• Minimalist.CyclicAgree.personSpec Minimalist.CyclicAgree.Geometry.addressee Person.firstInclusive = [Minimalist.CyclicAgree.Segment.pi, Minimalist.CyclicAgree.Segment.participant]
• Minimalist.CyclicAgree.personSpec Minimalist.CyclicAgree.Geometry.addressee Person.firstExclusive = [Minimalist.CyclicAgree.Segment.pi, Minimalist.CyclicAgree.Segment.participant]
• Minimalist.CyclicAgree.personSpec Minimalist.CyclicAgree.Geometry.standard Person.second = [Minimalist.CyclicAgree.Segment.pi, Minimalist.CyclicAgree.Segment.participant]

def Minimalist.CyclicAgree.mostSpecified : Geometry → Person

The most specified person under a given geometry.

Equations

• Minimalist.CyclicAgree.mostSpecified Minimalist.CyclicAgree.Geometry.standard = Person.first
• Minimalist.CyclicAgree.mostSpecified Minimalist.CyclicAgree.Geometry.addressee = Person.second

@[reducible, inline]

abbrev Minimalist.Probe.Articulation : 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

• Minimalist.Probe.Articulation = List Minimalist.CyclicAgree.Segment

def Minimalist.CyclicAgree.flatProbe : Probe.Articulation

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

Equations

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

def Minimalist.CyclicAgree.partialProbe : Probe.Articulation

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

Equations

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

def Minimalist.CyclicAgree.fullProbeStd : Probe.Articulation

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

Equations

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

def Minimalist.CyclicAgree.fullProbeAddr : Probe.Articulation

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

Equations

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

structure Minimalist.CyclicAgree.AgreementSystem : Type

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

[BR09] 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 : Probe.Articulation

@[implicit_reducible]

instance Minimalist.CyclicAgree.instDecidableEqAgreementSystem : DecidableEq AgreementSystem

Equations

• Minimalist.CyclicAgree.instDecidableEqAgreementSystem = Minimalist.CyclicAgree.instDecidableEqAgreementSystem.decEq

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

Equations

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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instReprAgreementSystem : Repr AgreementSystem

Equations

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

def Minimalist.CyclicAgree.instReprAgreementSystem.repr : AgreementSystem → ℕ → Std.Format

Equations

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

def Minimalist.CyclicAgree.swahili : AgreementSystem

Swahili/Abkhaz: flat probe, no PH sensitivity.

Equations

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

def Minimalist.CyclicAgree.basque : AgreementSystem

Basque/Georgian: partial probe, standard geometry.

Equations

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

def Minimalist.CyclicAgree.nishnaabemwin : AgreementSystem

Nishnaabemwin/Mohawk: full probe, addressee geometry.

Equations

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

def Minimalist.CyclicAgree.activeResidue (probe : Probe.Articulation) (goal : List Segment) : Probe.Articulation

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 [BR09]: partial matching of articulated probes drives agreement displacement.

Equations

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

inductive Minimalist.CyclicAgree.Controller : Type

Which argument controls the core agreement slot.

• ia : Controller
• ea : Controller

@[implicit_reducible]

instance Minimalist.CyclicAgree.instDecidableEqController : DecidableEq Controller

Equations

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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instReprController : Repr Controller

Equations

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

def Minimalist.CyclicAgree.instReprController.repr : Controller → ℕ → Std.Format

Equations

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

def Minimalist.CyclicAgree.eaAgrees (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : 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 Minimalist.CyclicAgree.agreementController (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : 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 Minimalist.CyclicAgree.agreementValue (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : Person

The person value that the core agreement slot realizes.

Equations

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

def Minimalist.CyclicAgree.AgreementSystem.controller (sys : AgreementSystem) (ea ia : Person) : Controller

Convenience: controller using an AgreementSystem.

Equations

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

def Minimalist.CyclicAgree.AgreementSystem.value (sys : AgreementSystem) (ea ia : Person) : Person

Convenience: agreement value using an AgreementSystem.

Equations

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

def Minimalist.CyclicAgree.cycleSegments (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : Probe.Articulation × Probe.Articulation

Which cycle valued the probe's remaining segments.

[BR09] §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 Minimalist.CyclicAgree.hasSecondCycleEffect (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : 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

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

def Minimalist.CyclicAgree.isInverseContext (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : 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

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

def Minimalist.CyclicAgree.isDirectContext (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : Bool

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

Equations

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

def Minimalist.CyclicAgree.AgreementSystem.isInverse (sys : AgreementSystem) (ea ia : Person) : Bool

Convenience: inverse using an AgreementSystem.

Equations

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

def Minimalist.CyclicAgree.eaIsLicensed (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : Bool

The Person-Licensing Condition (PLC).

[BR09] 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

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

theorem Minimalist.CyclicAgree.plc_violation_iff_inverse (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : 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.

Grounding in relativized search (Probe/Basic.lean)

An articulated probe is a family of flat relativized searches, one per segment, over the cyclically ordered token list: B&R's segments match independently, so cyclic expansion at the whole-probe level is first-visible-goal search at the per-segment level. The residue-based definitions above remain definitional — they are the paper's mechanism; the factorization is a result about it.

Cf. Studies/BejarRezac2003.lean for the 2003 precursor's second-cycle repair: formally distinct mechanisms — 2003 varies the goal order under one probe; cyclic expansion here varies the relativization (per segment) over one order.

def Minimalist.CyclicAgree.goalTokens (ea ia : Person) : List (Controller × Person)

The two arguments as φ-bearing goal tokens, in cyclic search order: the IA precedes the EA (cycle I before cycle II).

Equations

• Minimalist.CyclicAgree.goalTokens ea ia = [(Minimalist.CyclicAgree.Controller.ia, ia), (Minimalist.CyclicAgree.Controller.ea, ea)]

def Minimalist.CyclicAgree.segVisible (geom : Geometry) (s : Segment) (t : Controller × Person) : Bool

Visibility of an argument token to a probe segment s: the argument's person specification bears s (feature-relativized locality).

Equations

• Minimalist.CyclicAgree.segVisible geom s t = (Minimalist.CyclicAgree.personSpec geom t.2).contains s

def Minimalist.CyclicAgree.segProbe (geom : Geometry) (s : Segment) : Probe (Controller × Person)

A probe segment as a Probe over argument tokens.

Equations

• Minimalist.CyclicAgree.segProbe geom s = Minimalist.Probe.ofVis (Minimalist.CyclicAgree.segVisible geom s)

def Minimalist.CyclicAgree.segmentGoal (geom : Geometry) (ea ia : Person) (s : Segment) : Option (Controller × Person)

The goal a single probe segment Agrees with: the first argument in cyclic order whose specification bears the segment — a flat relativized Probe.search.

Equations

• Minimalist.CyclicAgree.segmentGoal geom ea ia s = (Minimalist.CyclicAgree.segProbe geom s).search (Minimalist.CyclicAgree.goalTokens ea ia)

theorem Minimalist.CyclicAgree.segmentGoal_eq_ea_iff (geom : Geometry) (ea ia : Person) (s : Segment) : segmentGoal geom ea ia s = some (Controller.ea, ea) ↔ (personSpec geom ia).contains s = false ∧ (personSpec geom ea).contains s = true

A segment finds the EA token iff the IA bypasses it (leaving it as active residue) and the EA bears it — cycle-II Agree.

theorem Minimalist.CyclicAgree.segmentGoal_eq_ia_iff (geom : Geometry) (ea ia : Person) (s : Segment) : segmentGoal geom ea ia s = some (Controller.ia, ia) ↔ (personSpec geom ia).contains s = true

A segment finds the IA token iff the IA bears it — cycle-I Agree.

theorem Minimalist.CyclicAgree.eaAgrees_iff_exists (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : eaAgrees geom probe ea ia = true ↔ ∃ s ∈ probe, (personSpec geom ia).contains s = false ∧ (personSpec geom ea).contains s = true

Existential characterization of the residue-based eaAgrees.

theorem Minimalist.CyclicAgree.eaIsLicensed_iff_segment_licensed (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : eaIsLicensed geom probe ea ia = true ↔ ∃ s ∈ probe, (segProbe geom s).Licensed (goalTokens ea ia) (Controller.ea, ea)

Main bridge: the EA is person-licensed (eaIsLicensed) iff some probe segment's flat relativized search (Probe.Licensed) over the cyclically ordered token list finds the EA token.

theorem Minimalist.CyclicAgree.plc_violation_iff_no_segment_licensed (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : isInverseContext geom probe ea ia = true ↔ ∀ s ∈ probe, ¬(segProbe geom s).Licensed (goalTokens ea ia) (Controller.ea, ea)

PLC violation ↔ no segment's search licenses the EA token — the inverse-context characterization restated through the search substrate.

theorem Minimalist.CyclicAgree.cycleSegments_eq_segmentGoal_filters (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : cycleSegments geom probe ea ia = (List.filter (fun (s : Segment) => segmentGoal geom ea ia s == some (Controller.ia, ia)) probe, List.filter (fun (s : Segment) => segmentGoal geom ea ia s == some (Controller.ea, ea)) probe)

Cycle decomposition through the search: cycle-I segments are those whose search finds the IA token; cycle-II segments those whose search finds the EA token. Second-cycle effects also factor through Probe.search.

inductive Minimalist.CyclicAgree.RepairStrategy : Type

Repair strategies for PLC violations in inverse contexts.

[BR09] §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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instDecidableEqRepairStrategy : DecidableEq RepairStrategy

Equations

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

@[implicit_reducible]

instance Minimalist.CyclicAgree.instReprRepairStrategy : Repr RepairStrategy

Equations

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

def Minimalist.CyclicAgree.instReprRepairStrategy.repr : RepairStrategy → ℕ → Std.Format

Equations

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

def Minimalist.CyclicAgree.needsRepair (sys : AgreementSystem) (ea ia : Person) : Bool

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

Repair is needed iff the context is inverse.

Equations

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

theorem Minimalist.CyclicAgree.std_participant_matches_decomposed (p : Person) : (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 Minimalist.CyclicAgree.std_third_singleton : personSpec Geometry.standard Person.third = [Segment.pi]

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

theorem Minimalist.CyclicAgree.std_spec_lengths : (personSpec Geometry.standard Person.first).length = 3 ∧ (personSpec Geometry.standard Person.second).length = 2 ∧ (personSpec Geometry.standard Person.third).length = 1

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

theorem Minimalist.CyclicAgree.std_first_entails_second (s : Segment) : s ∈ personSpec Geometry.standard Person.second → s ∈ personSpec Geometry.standard Person.first

Entailment: more specified persons' segments are supersets.

theorem Minimalist.CyclicAgree.std_second_entails_third (s : Segment) : s ∈ personSpec Geometry.standard Person.third → s ∈ personSpec Geometry.standard Person.second

theorem Minimalist.CyclicAgree.flat_no_residue (geom : Geometry) (ia : Person) : activeResidue flatProbe (personSpec geom ia) = []

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

theorem Minimalist.CyclicAgree.flat_ia_controls (geom : Geometry) (ea ia : Person) : agreementController geom flatProbe ea ia = Controller.ia

Flat probe: IA always controls — no PH effects.

theorem Minimalist.CyclicAgree.flat_all_inverse (geom : Geometry) (ea ia : Person) : isInverseContext geom flatProbe ea ia = true

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

theorem Minimalist.CyclicAgree.partial_geometry_invariant (ea ia : Person) : 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 Minimalist.CyclicAgree.basque_3_1 : basque.value Person.third Person.first = Person.first

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

theorem Minimalist.CyclicAgree.basque_2_1 : basque.value Person.second Person.first = Person.first

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

theorem Minimalist.CyclicAgree.basque_1_2 : basque.value Person.first Person.second = Person.second

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

theorem Minimalist.CyclicAgree.basque_3_2 : basque.value Person.third Person.second = Person.second

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

theorem Minimalist.CyclicAgree.basque_1_3 : basque.value Person.first Person.third = Person.first

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

theorem Minimalist.CyclicAgree.basque_2_3 : basque.value Person.second Person.third = Person.second

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

theorem Minimalist.CyclicAgree.basque_3_3 : basque.value Person.third Person.third = Person.third

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

theorem Minimalist.CyclicAgree.basque_sap_ia_inverse (ea : Person) : basque.isInverse ea Person.first = true ∧ basque.isInverse ea Person.second = true

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

theorem Minimalist.CyclicAgree.basque_3p_ia_direct (ea : Person) (h : ea.IsSAP) : isDirectContext Geometry.standard partialProbe ea Person.third = true

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

theorem Minimalist.CyclicAgree.basque_3_3_inverse : basque.isInverse Person.third Person.third = true

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

theorem Minimalist.CyclicAgree.nish_3_2 : nishnaabemwin.value Person.third Person.second = Person.second

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

theorem Minimalist.CyclicAgree.nish_1_2 : nishnaabemwin.value Person.first Person.second = Person.second

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

theorem Minimalist.CyclicAgree.nish_3_1 : nishnaabemwin.value Person.third Person.first = Person.first

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

theorem Minimalist.CyclicAgree.nish_2_1 : nishnaabemwin.value Person.second Person.first = Person.second

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

theorem Minimalist.CyclicAgree.nish_1_3 : nishnaabemwin.value Person.first Person.third = Person.first

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

theorem Minimalist.CyclicAgree.nish_2_3 : nishnaabemwin.value Person.second Person.third = Person.second

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

theorem Minimalist.CyclicAgree.nish_3_3 : nishnaabemwin.value Person.third Person.third = Person.third

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

theorem Minimalist.CyclicAgree.nish_2p_ia_inverse (ea : Person) : nishnaabemwin.isInverse ea Person.second = true

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

theorem Minimalist.CyclicAgree.nish_3p_ia_sap_ea_direct : isDirectContext Geometry.addressee fullProbeAddr Person.first Person.third = true ∧ isDirectContext Geometry.addressee fullProbeAddr Person.second Person.third = true

Nishnaabemwin: 3P IA with SAP EA → direct.

theorem Minimalist.CyclicAgree.nish_3_1_inverse : nishnaabemwin.isInverse Person.third Person.first = true

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

theorem Minimalist.CyclicAgree.nish_3_3_inverse : nishnaabemwin.isInverse Person.third Person.third = true

Nishnaabemwin: 3→3 is inverse.

theorem Minimalist.CyclicAgree.georgian_1_3_second_cycle : hasSecondCycleEffect Geometry.standard partialProbe Person.first Person.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 Minimalist.CyclicAgree.georgian_no_second_cycle_sap_ia (ea : Person) : hasSecondCycleEffect Geometry.standard partialProbe ea Person.first = false ∧ hasSecondCycleEffect Geometry.standard partialProbe ea Person.second = false

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

theorem Minimalist.CyclicAgree.nish_2_1_second_cycle : hasSecondCycleEffect Geometry.addressee fullProbeAddr Person.second Person.first = true

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

theorem Minimalist.CyclicAgree.nish_2_1_cycle_segments : (cycleSegments Geometry.addressee fullProbeAddr Person.second Person.first).2 = [Segment.addressee]

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

theorem Minimalist.CyclicAgree.same_person_ia_controls (geom : Geometry) (probe : Probe.Articulation) (p : Person) : 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 Minimalist.CyclicAgree.most_specified_controls_vs_third_std : agreementValue Geometry.standard fullProbeStd (mostSpecified Geometry.standard) Person.third = mostSpecified Geometry.standard ∧ agreementValue Geometry.standard fullProbeStd Person.third (mostSpecified Geometry.standard) = mostSpecified Geometry.standard

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

theorem Minimalist.CyclicAgree.most_specified_controls_vs_third_addr : agreementValue Geometry.addressee fullProbeAddr (mostSpecified Geometry.addressee) Person.third = mostSpecified Geometry.addressee ∧ agreementValue Geometry.addressee fullProbeAddr Person.third (mostSpecified Geometry.addressee) = mostSpecified Geometry.addressee

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

theorem Minimalist.CyclicAgree.direct_inverse_exhaustive (geom : Geometry) (probe : Probe.Articulation) (ea ia : Person) : (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 Minimalist.CyclicAgree.partial_probe_sap_ia_is_inverse (ea : Person) : isInverseContext Geometry.standard partialProbe ea Person.first = true ∧ isInverseContext Geometry.standard partialProbe ea Person.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 Minimalist.CyclicAgree.partial_probe_3p_ia_sap_ea_is_direct : isDirectContext Geometry.standard partialProbe Person.first Person.third = true ∧ isDirectContext Geometry.standard partialProbe Person.second Person.third = true

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

theorem Minimalist.CyclicAgree.sap_ia_indexed_via_inverse (p : Person) (h : p.IsSAP) (ea : Person) : 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 Minimalist.CyclicAgree.inverseCount (sys : AgreementSystem) : ℕ

Count inverse contexts in a 3×3 paradigm.

Equations

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

theorem Minimalist.CyclicAgree.swahili_all_inverse : inverseCount swahili = 9

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

theorem Minimalist.CyclicAgree.basque_inverse_count : inverseCount basque = 7

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

theorem Minimalist.CyclicAgree.nish_inverse_count : inverseCount nishnaabemwin = 6

Nishnaabemwin (full): 6 inverse, 3 direct.

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

More articulated probes yield more direct contexts.