Mam Agreement Fragment

Agreement morphology and pronoun realization data for San Juan Atitán Mam (SJA Mam, Mayan), following [Sco23]. SJA Mam has morphologically tripartite agreement alignment — S, A, and O each trigger distinct verbal marking (Scott's ch. 3, "Object licensing and agreement: SJA Mam is a tripartite high-abs language") — realized through two paradigms: Set A (ERG) prefixes on Voice cross-referencing the transitive agent, and Set B (ABS) preverbal markers on Infl cross-referencing the absolutive (intransitive S). Transitive objects are cross-referenced by neither set: they co-occur with default Set B (tz'=) and require full overt pronouns, though some speakers accept agreeing Set B for objects as a more formal variant ([Sco23] ch. 3, ex. 156).

Main declarations

• Mam.setAExponent, Mam.setBExponent: the Set A (ERG) and Set B (ABS) exponent tables ([Sco23] Tables 2.8, 3.5).
• Mam.ArgPosition with .case, .IsPhiAgreed, .CanBeReduced: argument positions, their tripartite case values, φ-agreement status, and reduction eligibility.
• Mam.PhiDimension with .Copied, agreedDimensions, baseDimensions, encliticDimensions: the φ-feature redundancy calculus behind pronoun reduction.
• Mam.realizedPronoun: pronoun realization by argument position, as a selection among the shared PersonalPronoun entries.
• Mam.caseInventory: the {ERG, ACC, ABS} inventory, validated against [Bla94b]'s hierarchy.
• Mam.absPosition: HIGH-ABS morpheme placement (extraction marking lives in Mam/Extraction.lean).

Implementation notes

This fragment encodes Scott's tripartite analysis of SJA Mam specifically — an analytical contribution using a high-abs / Voice Licensing / Ergative Extraction Constraint framework ([Sco23] ch. 3 §3.4) to argue for tripartite case (ERG, ACC, ABS) even though Mam lacks independent DP case morphology; case is visible only through agreement. Other Mam dialects (notably Ixtahuacán Mam, described in England 1983b and used by [ZM17] §4-5) are characterized as ergative with a neutral pattern in aspectless dependent clauses — not tripartite; per [ZM17] §4 (p. 237), "Ch'orti' is the only Mayan language that exhibits three sets of pronominal markers", the canonical tripartite Mayan language under that framing. Per [Sco23] §1.2.4 and Table 1.2 (citing Simon 2019), Mam dialects vary substantially, so the SJA analysis may not extend to Ixtahuacán Mam.

Case is not dependent case ([Sco23]; cf. [Woo97], [Dea24]): ERG is inherent case from Voice, ACC structural case from Voice (object licensing, low-abs syntax), ABS structural case from Infl (high-abs morphology, for intransitive S). In transitives, Infl's φ-probe is blocked by transitive VoiceP and default Set B (∅/tz'=) surfaces. Person-number cells are the canonical φ-cells Agreement.Cell (Syntax/Agreement/Paradigm.lean), built with Agreement.Cell.pn (the six-cell inventory Agreement.Cell.pnCells); per-cell pronoun feature values live in Mam.ScottFeatures (Fragments/Mayan/Mam/Pronouns.lean).

Agreement marker paradigms

def Mam.setAExponent : Mayan.ExponentTable

Set A (ERG) markers cross-referencing the transitive agent ([Sco23] Table 2.8); t- is syncretic for 2/3SG, ky- for 2/3PL.

Equations

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

def Mam.setBExponent : Mayan.ExponentTable

Set B (ABS) markers ([Sco23] Table 3.5). The 2/3SG form tz'= is the Elsewhere default: it realizes both real 2/3SG intransitive-S agreement and default Set B in transitives when Infl's probe is blocked by VoiceP. Per Scott's DM analysis 2SG and 3SG are not specific Vocabulary Items but surface via Elsewhere fallback (see setBSpecificCells).

Equations

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

def Mam.setBSpecificCells : List Agreement.Cell

The four Set B cells with specific Vocabulary Items ([Sco23]); 2SG and 3SG fall through to the Elsewhere entry.

Equations

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

def Mam.defaultSetB : String

The Elsewhere Set B marker, surfacing in transitives when Infl's probe is blocked and for 2/3SG intransitive S.

Equations

• Mam.defaultSetB = "tz'="

Argument positions and agreement status

@[reducible, inline]

abbrev Mam.ArgPosition : Type

Argument positions, aliased to the canonical Features.Prominence.ArgumentRole (S/A/P/R/T) ([Sco23] ch. 3).

Equations

• Mam.ArgPosition = Features.Prominence.ArgumentRole

@[reducible, inline]

abbrev Mam.ArgPosition.case : ArgPosition → Case

Tripartite case assignment: Mayan.ergCaseMam (A → ERG inherent from Voice, P → ACC structural from Voice, S → ABS structural from Infl; [Sco23] ch. 3 §3.4).

Equations

• Mam.ArgPosition.case = Mayan.ergCaseMam

def Mam.ArgPosition.IsPhiAgreed : ArgPosition → Prop

Whether a position triggers φ-Agree. A is probed by Voice (→ Set A), S by Infl (→ Set B); the transitive patient is not, because Infl's φ-probe has a disjunctive satisfaction condition [SAT: φ or Voice_TR] and stops at transitive Voice before copying features, so default Set B surfaces. R/T default to participating (not modeled).

Equations

• Mam.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.A = True
• Mam.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.P = False
• Mam.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.S = True
• Mam.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.R = True
• Mam.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.T = True

@[implicit_reducible]

instance Mam.instDecidablePredArgPositionIsPhiAgreed : DecidablePred ArgPosition.IsPhiAgreed

Equations

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

Pronoun reduction eligibility

def Mam.ArgPosition.CanBeReduced (pos : ArgPosition) : Prop

Whether a pronoun here is eligible for reduction (≡ φ-agreement). Under Scott's analysis (ch. 4 §4.4.3), agreed-with first-person pronouns undergo an impoverishment rule deleting [±singular] in the context of [+author]^F (F = agreed-with), bleeding the base morphemes qin [+author,+sg] and qo [+author,−sg] and leaving only the disagreement enclitic =i; non-first-person pronouns are not reduced, their subject/possessor forms matching the independent ones ([Sco23] Table 4.25, p. 200). Only agreed-with positions are eligible; whether reduction actually applies depends on person (see realizedPronoun).

Equations

• pos.CanBeReduced = pos.IsPhiAgreed

@[implicit_reducible]

instance Mam.instDecidablePredArgPositionCanBeReduced : DecidablePred ArgPosition.CanBeReduced

Equations

• Mam.instDecidablePredArgPositionCanBeReduced pos = id inferInstance

Per-position verification

theorem Mam.A_case : ArgPosition.case Features.Prominence.ArgumentRole.A = Case.erg

Agent gets ERG (inherent, from Voice).

theorem Mam.P_case : ArgPosition.case Features.Prominence.ArgumentRole.P = Case.acc

Patient gets ACC (structural, from Voice).

theorem Mam.S_case : ArgPosition.case Features.Prominence.ArgumentRole.S = Case.abs

Intransitive S gets ABS (structural, from Infl).

theorem Mam.tripartite_alignment : ArgPosition.case Features.Prominence.ArgumentRole.A ≠ ArgPosition.case Features.Prominence.ArgumentRole.P ∧ ArgPosition.case Features.Prominence.ArgumentRole.A ≠ ArgPosition.case Features.Prominence.ArgumentRole.S ∧ ArgPosition.case Features.Prominence.ArgumentRole.P ≠ ArgPosition.case Features.Prominence.ArgumentRole.S

Three distinct underlying cases (morphologically tripartite), inherited from Alignment.tripartite_distinguishes_all.

theorem Mam.reduction_eligible_iff_phi_agreed (pos : ArgPosition) : pos.CanBeReduced ↔ pos.IsPhiAgreed

Reduction eligibility coincides with φ-agreement — reflexivity, since CanBeReduced := IsPhiAgreed.

Case inventory ([Bla94b])

def Mam.caseInventory : Finset Case

The case inventory realized by the core positions: {ERG, ACC, ABS}.

Equations

• Mam.caseInventory = (List.map Mam.ArgPosition.case Features.Prominence.ArgumentRole.core).toFinset

theorem Mam.inventory_covers_positions (p : Features.Prominence.ArgumentRole) : p ∈ Features.Prominence.ArgumentRole.core → ArgPosition.case p ∈ caseInventory

The inventory covers all argument positions.

Pronoun internal structure ([Sco23] ch. 4)

inductive Mam.PhiDimension : Type

The three φ-dimensions of the SJA Mam pronominal system ([Sco23] Table 4.4, after [Har16a]'s bivalent features): [±author], [±participant], [±singular]. This enum names the dimensions for the redundancy calculus below; per-cell values live in Mam.ScottFeatures (Fragments/Mayan/Mam/Pronouns.lean).

• author : PhiDimension
• participant : PhiDimension
• singular : PhiDimension

@[implicit_reducible]

instance Mam.instDecidableEqPhiDimension : DecidableEq PhiDimension

Equations

• Mam.instDecidableEqPhiDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mam.instReprPhiDimension : Repr PhiDimension

Equations

• Mam.instReprPhiDimension = { reprPrec := Mam.instReprPhiDimension.repr }

def Mam.instReprPhiDimension.repr : PhiDimension → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Mam.instReprPhiDimension.repr Mam.PhiDimension.author prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PhiDimension.author")).group prec✝
• Mam.instReprPhiDimension.repr Mam.PhiDimension.singular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.PhiDimension.singular")).group prec✝

def Mam.agreedDimensions : List PhiDimension

Dimensions referenced by Set A and Set B agreement Vocabulary Items — [±author] and [±singular] only ([Sco23] Tables 4.7-4.8); agreement never copies [±participant].

Equations

• Mam.agreedDimensions = [Mam.PhiDimension.author, Mam.PhiDimension.singular]

def Mam.baseDimensions : List PhiDimension

Dimensions realized by the pronominal base morphemes qin [+author,+sg] and qo [+author,−sg] (Table 4.10).

Equations

• Mam.baseDimensions = [Mam.PhiDimension.author, Mam.PhiDimension.singular]

def Mam.encliticDimensions : List PhiDimension

Dimensions whose disagreement the =i enclitic realizes ([Noy92]; [Sco23] §4.3.3): [±author] and [±participant].

Equations

• Mam.encliticDimensions = [Mam.PhiDimension.author, Mam.PhiDimension.participant]

def Mam.PhiDimension.Copied (d : PhiDimension) : Prop

A dimension is copied back to the probe by agreement.

Equations

• d.Copied = (d ∈ Mam.agreedDimensions)

@[implicit_reducible]

instance Mam.instDecidablePredPhiDimensionCopied : DecidablePred PhiDimension.Copied

Equations

• Mam.instDecidablePredPhiDimensionCopied d = id inferInstance

theorem Mam.base_is_redundant (d : PhiDimension) : d ∈ baseDimensions → d.Copied

The pronominal base is fully redundant under agreement — every dimension it realizes is copied, the configuration in which impoverishment bleeds base insertion ([Sco23] §4.4).

theorem Mam.enclitic_survives : ¬∀ d ∈ encliticDimensions, d.Copied

The =i enclitic is not fully redundant: [±participant] is never copied by agreement — so the enclitic survives reduction.

def Mam.realizedPronoun (pos : ArgPosition) (c : PronCell) : Option PersonalPronoun

Pronoun realization by argument position — the nominative alignment of reduction ([Sco23] (3)/(8)). φ-agreed positions (A, S, and possessors) take the subject/possessor series, the unagreed object the independent series. The impoverishment rule [±singular] → ∅ / [+author]^F (ex. 84/94) targets [+author] under the agreed-with diacritic F, bleeding the bases qin/qo, so agreed-with first person surfaces as bare =i (∅ for 1PL.INCL) while everything else keeps its independent form. Realization selects among the shared PersonalPronoun entries, not a separate form classification.

Equations

• Mam.realizedPronoun pos c = if pos.IsPhiAgreed then Mam.subjPoss c else Mam.independent c

theorem Mam.first_A_reduced : realizedPronoun Features.Prominence.ArgumentRole.A PronCell.firstSg = some iDisagr

1SG agent: reduced to the bare disagreement enclitic (base bled by impoverishment).

theorem Mam.first_S_reduced : realizedPronoun Features.Prominence.ArgumentRole.S PronCell.firstSg = some iDisagr

1SG intransitive subject: likewise reduced (Set B agreement).

theorem Mam.first_P_full : realizedPronoun Features.Prominence.ArgumentRole.P PronCell.firstSg = some qini

1SG patient: the full independent pronoun qini (no agreement → no F diacritic → no impoverishment).

theorem Mam.second_A_unreduced : realizedPronoun Features.Prominence.ArgumentRole.A PronCell.secondSg = independent PronCell.secondSg

2SG agent: unreduced — =i IS the independent 2SG form (Scott's fn. 2), so the agreed-with cell coincides with the independent one.

theorem Mam.third_A_full : realizedPronoun Features.Prominence.ArgumentRole.A PronCell.thirdPl = some qa

3PL agent: full qa (impoverishment does not apply to [−author]).

theorem Mam.first_A_vs_P : realizedPronoun Features.Prominence.ArgumentRole.A PronCell.firstSg ≠ realizedPronoun Features.Prominence.ArgumentRole.P PronCell.firstSg

The nominative-alignment contrast: the same 1SG argument is =i as agent but qini as patient.

theorem Mam.first_vs_nonfirst_asymmetry : realizedPronoun Features.Prominence.ArgumentRole.A PronCell.firstSg ≠ realizedPronoun Features.Prominence.ArgumentRole.A PronCell.thirdSg ∧ realizedPronoun Features.Prominence.ArgumentRole.S PronCell.firstSg ≠ realizedPronoun Features.Prominence.ArgumentRole.S PronCell.thirdSg

Agreed-with first person differs from agreed-with third person — the impoverishment rule targets [+author] only.

theorem Mam.patient_takes_independent (c : PronCell) : realizedPronoun Features.Prominence.ArgumentRole.P c = independent c

The unagreed object position realizes the independent series, for every cell — person is irrelevant without the F diacritic.

Mayan absolutive parameter

def Mam.absPosition : Mayan.ABSPosition

HIGH-ABS: Set B (absolutive) markers sit pre-stem on Infl, right after the aspect marker — template ASP-ABS-ERG-ROOT-SUFFIX ([Sco23] §2.5.1).

Equations

• Mam.absPosition = Mayan.ABSPosition.high

theorem Mam.mam_case_locus : Mayan.toCaseLocus absPosition = Mayan.CaseLocus.absNom

HIGH-ABS yields ABS=NOM case locus: Infl assigns case to the absolutive argument ([Sco23], §3.3).

def Mam.setALinearity : Mayan.MarkerLinearity

Set A linearity: prefixal (per [Sco23] ch. 2; pan-Mayan).

Equations

• Mam.setALinearity = Mayan.MarkerLinearity.prefixal

def Mam.setBLinearity : Mayan.MarkerLinearity

Set B linearity: prefixal (HIGH-ABS Mam morphology; pre-stem on Infl, per [Sco23] §2.5.1).

Equations

• Mam.setBLinearity = Mayan.MarkerLinearity.prefixal

Marker verification

theorem Mam.setA_1sg : Agreement.Paradigm.realize setAExponent (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = some "n-/w-"

Set A 1SG marker.

theorem Mam.setA_3sg : Agreement.Paradigm.realize setAExponent (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = some "t-"

Set A 3SG marker is "t-" (the default singular Set A — syncretic with 2SG).

theorem Mam.setB_1sg : Agreement.Paradigm.realize setBExponent (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = some "chin"

Set B 1SG marker is "chin".

theorem Mam.setB_3sg : Agreement.Paradigm.realize setBExponent (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = some defaultSetB

Set B 3SG marker is the default "tz'=".

theorem Mam.erg_1sg_from_phi : Agreement.Paradigm.realizeFor setAExponent { form := "", cat := UD.UPOS.PRON, features := { number := some UD.Number.Sing, person := some UD.Person.first } } = some "n-/w-"

A controller's φ-features index the agreement paradigm directly: the Set A table is keyed by canonical φ-cells, so a pronoun's Word.agrCell drives realization in one shared feature space ([Cor98]; [Sco23] Ch. 2). The realizational account (impoverishment, Elsewhere; [Sco23] Ch. 4) stays in the study.