Mam Agreement Fragment [Sco23]

[Dea24] [Woo97] [Bla94b]

Agreement morphology and pronoun realization data for San Juan Atitán Mam (SJA Mam), the dialect analyzed in [Sco23]. Per Scott's Chapter 3 (titled "Object licensing and agreement: SJA Mam is a tripartite high-abs language"), SJA Mam exhibits morphologically tripartite agreement alignment: S, A, and O each trigger distinct marking patterns on the verb.

Dialect-specificity and the analytical contrast

This fragment encodes Scott's analysis of SJA Mam specifically. Other Mam dialects (notably Ixtahuacán Mam, the variety described in England 1983b and used by [ZM17] §4-5) have been characterized as ergative with a neutral pattern in aspectless dependent clauses — NOT tripartite. Per Zavala 2017 §4 (p. 237), "Ch'orti' is the only Mayan language that exhibits three sets of pronominal markers" — making Ch'orti' the canonical tripartite Mayan language under that framing.

Scott's tripartite analysis of SJA Mam is an analytical contribution that uses a high-abs / Voice Licensing / Ergative Extraction Constraint framework (her ch. 3 §3.4) to argue for tripartite case (ERG, ACC, ABS) even though Mam lacks independent DP case morphology. Per Scott §1.2.4 (Mam dialect variation, p. 11) and Table 1.2 (Mam dialect groups, citing Simon 2019), Mam dialects vary substantially; the SJA Mam analysis may not extend directly to Ixtahuacán Mam.

The System

Mam has two agreement paradigms on the verb:

• Set A (ERG): prefixes on Voice cross-referencing the transitive agent
• Set B (ABS): preverbal markers on Infl cross-referencing the absolutive argument (intransitive S). In transitives, Infl's φ-probe is blocked by transitive VoiceP and default Set B (∅/tz'=) appears instead.

In the default construction, transitive objects are not cross-referenced by either set — they co-occur with default Set B (tz'=) and require full overt pronouns. However, some speakers accept agreeing Set B for objects as a more formal variant ([Sco23], ch. 3, ex. 156).

Case Licensing (per Scott's analysis)

Case is NOT assigned via dependent case. Instead:

• ERG: 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)

This gives a tripartite underlying Case system (ERG, ACC, ABS) despite Mam having no independent case morphology on DPs — case is visible only through agreement patterns. This tripartite analysis is dialect-specific to SJA Mam per Scott; alternative analyses (for other Mam dialects or under different theoretical frameworks) characterize Mam as ergative with neutral patterns in dependent clauses (England 1983b; [ZM17] §4-5).

Argument Positions

Position	Case	Agreement	Pronoun
A (transitive agent)	ERG (from Voice)	Set A	reduced/null
S (intransitive subj)	ABS (from Infl)	Set B	reduced/null
P (transitive patient)	ACC (from Voice)	default Set B	overt

def Mam.setAExponent : Mayan.ExponentTable

Set A (ERG) markers per cell: prefixes/proclitics on the verb that cross-reference the transitive agent ([Sco23], Table 2.8). All six cells have distinct exponents (with t- syncretism for 2sg/3sg and ky- syncretism for 2pl/3pl).

Equations

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

def Mam.setBExponent : Mayan.ExponentTable

Set B (ABS) markers per cell ([Sco23], Table 3.5). The 2/3SG form tz'= is the default — it appears both for real agreement with a 2/3SG intransitive S and for default Set B in transitives when Infl's probe is blocked by VoiceP.

Per Scott's DM analysis, 2sg and 3sg are NOT specific entries; they surface via the Elsewhere fallback. The total function below returns "tz'=" for both, but downstream Vocabulary construction should treat them as derived from the Elsewhere entry. See setBSpecificCells for the cells that have actual specific Vocabulary Items in the DM analysis.

Equations

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

def Mam.setBSpecificCells : List Agreement.Cell

The four Set B cells that have specific Vocabulary Items (per Scott's DM analysis). 2sg and 3sg are NOT included — they fall through to the Elsewhere entry.

Equations

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

def Mam.defaultSetB : String

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

Equations

• Mam.defaultSetB = "tz'="

@[reducible, inline]

abbrev Mam.ArgPosition : Type

Argument positions in a Mam clause ([Sco23] ch. 3). Aliased to the canonical Features.Prominence.ArgumentRole (S/A/P/R/T) so cross-Mayan and cross-framework code shares one inventory. Use the canonical constructor names .A / .P / .S directly.

Equations

• Mam.ArgPosition = Features.Prominence.ArgumentRole

@[reducible, inline]

abbrev Mam.ArgPosition.case : ArgPosition → Case

The case each argument position receives. Definitionally equal to Mayan.ergCaseMam, which derives from Alignment.tripartite.assignCase in Syntax/Case/Alignment.lean: A → ERG (inherent from Voice), P → ACC (structural from Voice), S → ABS (structural from Infl). The three distinct cases are tripartite alignment per Scott's analysis (ch. 3 §3.4).

Equations

• Mam.ArgPosition.case = Mayan.ergCaseMam

def Mam.ArgPosition.IsPhiAgreed : ArgPosition → Prop

Does this argument position participate in φ-Agree?

Agent: Voice probes for φ, finds agent in Spec,VoiceP → Set A Intransitive S: Infl probes for φ, finds S → Set B Patient: Infl's φ-probe has a disjunctive satisfaction condition [SAT: φ or Voice_TR]. In transitives, the probe encounters transitive Voice and stops — no φ-features are copied, and default Set B (the Elsewhere form) surfaces. Ditransitive 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.

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

Can a pronoun in this argument position undergo reduction?

Scott's analysis (ch. 4, §4.4.3): first person pronouns in agreed-with positions are reduced via an impoverishment rule that deletes [±singular] in the context of [+author]^F (where F marks that the feature has been agreed with). This bleeds insertion of the pronominal base morphemes qin ([+author,+singular]) and qo ([+author,-singular]), leaving only the disagreement enclitic =i.

Non-first person pronouns are NOT reduced — their subj/poss forms are identical to their independent forms (Table 4.25, p. 200). Whether actual reduction occurs depends on person (see realizedPronoun), but only agreed-with positions are eligible.

Equations

• pos.CanBeReduced = pos.IsPhiAgreed

@[implicit_reducible]

instance Mam.instDecidablePredArgPositionCanBeReduced : DecidablePred ArgPosition.CanBeReduced

Equations

• Mam.instDecidablePredArgPositionCanBeReduced pos = id inferInstance

def Mam.mamArgPositions : List ArgPosition

The three monotransitive argument positions.

Equations

• Mam.mamArgPositions = [Features.Prominence.ArgumentRole.A, Features.Prominence.ArgumentRole.P, Features.Prominence.ArgumentRole.S]

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. Inherits from Alignment.tripartite_distinguishes_all via the substrate connection.

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

Reduction eligibility ≡ φ-agreement: an argument position is eligible for pronoun reduction iff it triggers agreement on the verb. By CanBeReduced := IsPhiAgreed, this is reflexivity.

def Mam.caseInventory : Finset Case

Mam case inventory, derived from argument position case values.

Equations

• Mam.caseInventory = {Case.erg, Case.acc, Case.abs}

theorem Mam.inventory_covers_positions (p : ArgPosition) : p ∈ mamArgPositions → p.case ∈ caseInventory

The inventory covers all argument positions.

inductive Mam.PhiDimension : Type

φ-dimensions of the SJA Mam pronominal system ([Sco23] Table 4.4, adopting [Har16a]'s bivalent features): [±author], [±participant], [±singular]. Per-cell values live in Mam.ScottFeatures (Fragments/Mayan/Mam/Pronouns.lean, where the disagreement distribution of the =i enclitic is verified); this enum names the dimensions, for the redundancy calculus below.

• 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/Set B agreement vocabulary items: only [±author] and [±singular] (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 (§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 ([Sco23], her (3)/(8): nominative alignment of reduction). φ-agreed positions (A, S — and possessors) take the subject/possessor series; the unagreed object position takes the independent series. The impoverishment rule (ex. 84/94) [±singular] → ∅ / [+author]^F targets [+author] features bearing the agreed-with diacritic F, bleeding insertion of the bases qin/qo — so agreed-with first person surfaces as bare =i (or ∅ for 1PL.INCL), while everything else keeps its independent form. Realization is selection among the API's 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.

def Mam.absPosition : Mayan.ABSPosition

Mam is HIGH-ABS: Set B (absolutive) markers appear pre-stem on Infl, immediately following the aspect marker. Morpheme 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

def Mam.extractionStrategy : Extraction.ExtractionMarkingStrategy

Mam's extraction strategy: AF morphology is productive in SJA Mam ([Sco23] §2.5.4.1 ex. 169 + §2.7.1 syntactic ergativity). The construction combines the antipassive suffix -(a)n with the AF-specific suffix -ta (e.g., b'yo-n-ta 'hit-AP-AF'), making SJA Mam's AF morphologically distinct from K'iche''s (which uses bare antipassive -n in AF contexts per [Mon17] Lesson 22 — no extra AF morpheme).

For the cross-Mayan typology, we mark the strategy as dedicatedMorpheme (the descriptive surface category) to parallel Q'anjob'al/Kaqchikel/K'iche'. The analytical claim that AF is an SSAL repair (Erlewine-line) lives in Studies/Erlewine2016.lean; rival accounts (Coon-Mateo Pedro-Preminger absolutive licensing, Coon-Keine Feature Gluttony) are not encoded in the typology enum.

Language: "Mam (SJA)". Notes: AF (-(a)n + -ta) for A-extraction; HIGH-ABS tripartite Mam (Scott 2023 §2.5.4.1).

Equations

• Mam.extractionStrategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme

def Mam.extractionMarkedPositions : List Extraction.ExtractionTarget

Equations

• Mam.extractionMarkedPositions = [Extraction.ExtractionTarget.subject]

def Mam.extractionDistinguishesPosition : Bool

Equations

• Mam.extractionDistinguishesPosition = true

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: a 1sg agent selects its first-person-singular ergative prefix. The Set A table (setAExponent) is keyed by canonical φ-cells, so a pronoun's Word.agrCell drives agreement realization in one shared feature space ([Cor98]; [Sco23] Ch. 2). The realizational account (impoverishment / Elsewhere; [Sco23] Ch. 4) is theory and stays in the study.