Differential Indexing

[Ais03] [Jus24] [Has19] [Sie04] [Pre14] [Has21]

Formalizes the typological survey of Just, E. (2024), A structural and functional comparison of differential A and P indexing (Linguistics 62(2): 295–321), and connects it to [Ais03]'s DOM profiles (Features/Prominence), [Pre14]'s φ-geometry (Syntax/Minimalist/Phi/), and the Kaqchikel, Basque, Georgian, and Hungarian fragments.

Flagging = case morphology on the NP; indexing = verbal agreement/cross-referencing ([Has19], Just §2). The same prominence scales (person, animacy, definiteness) govern both, with opposite polarity by role (Just §4.2, p. 311): P indexing targets prominent Ps, A indexing targets non-prominent As. Both follow from a single principle (Just §6, p. 315): prominent arguments are indexed more readily regardless of role; A defaults prominent, P does not.

Main declarations

• IndexingFragment: per-language differential-indexing profile, extending DifferentialMarkingProfile (channel .indexing)
• pIndexingLanguages, aIndexingLanguages: Just (2024) Tables 1–2
• mirror_image_universal: every language targets the role-appropriate end of each conditioning scale
• person_dominates_P / person_dominates_A: person is the most frequent conditioning factor for both roles
• personLevel_matches_participant: Just's SAP/3rd split is [Pre14]'s [±participant]
• basque_fragment_matches_survey, georgian_fragment_matches_survey, hungarian_conjugation_split: fragment paradigms ground the survey rows

inductive Aissen2003.IndexingPersonLevel : Type

Person prominence for differential indexing.

The person scale for indexing is a binary split between speech act participants (SAP: 1st/2nd person) and non-participants (3rd person). This mirrors [Pre14]'s [±participant] feature decomposition.

This is coarser than Person (1st > 2nd > 3rd), which is needed for scenario splits. The binary split suffices for indexing because indexing does not distinguish 1st from 2nd.

• sap : IndexingPersonLevel

  Speech act participants: 1st and 2nd person

• third : IndexingPersonLevel

  Non-participants: 3rd person

@[implicit_reducible]

instance Aissen2003.instDecidableEqIndexingPersonLevel : DecidableEq IndexingPersonLevel

Equations

• Aissen2003.instDecidableEqIndexingPersonLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aissen2003.instReprIndexingPersonLevel : Repr IndexingPersonLevel

Equations

• Aissen2003.instReprIndexingPersonLevel = { reprPrec := Aissen2003.instReprIndexingPersonLevel.repr }

def Aissen2003.instReprIndexingPersonLevel.repr : IndexingPersonLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aissen2003.instInhabitedIndexingPersonLevel : Inhabited IndexingPersonLevel

Equations

• Aissen2003.instInhabitedIndexingPersonLevel = { default := Aissen2003.instInhabitedIndexingPersonLevel.default }

def Aissen2003.IndexingPersonLevel.rank : IndexingPersonLevel → ℕ

Rank on the indexing person scale: SAP (1) > 3rd (0).

Equations

• Aissen2003.IndexingPersonLevel.sap.rank = 1
• Aissen2003.IndexingPersonLevel.third.rank = 0

def Aissen2003.IndexingPersonLevel.all : List IndexingPersonLevel

All indexing person levels.

Equations

• Aissen2003.IndexingPersonLevel.all = [Aissen2003.IndexingPersonLevel.sap, Aissen2003.IndexingPersonLevel.third]

theorem Aissen2003.indexing_person_rank_injective (a b : IndexingPersonLevel) (h : a.rank = b.rank) : a = b

structure Aissen2003.IndexingFragmentextends Features.Prominence.DifferentialMarkingProfile : Type

A differential indexing fragment for a single language.

Extends DifferentialMarkingProfile with language metadata and per-dimension marking predicates. The 2D marks predicate is computed from animacyIndexed and definitenessIndexed by the mk' constructor, and the channel is always .indexing.

For P indexing: true at a level means "P arguments at this level ARE indexed." The expectation (Just §4.2) is that P indexing targets the prominent end of each scale.

For A indexing: true at a level means "A arguments at this level ARE indexed." The expectation is that A indexing targets the non-prominent end.

• name : String
• role : ArgumentRole
• channel : MarkingChannel
• marks : AnimacyLevel → DefinitenessLevel → Bool
• iso639 : String

  ISO 639-3 code

• family : String

  Language family

• personIndexed : IndexingPersonLevel → Bool

  Which person levels trigger indexing

• animacyIndexed : Features.Prominence.AnimacyLevel → Bool

  Which animacy levels trigger indexing

• definitenessIndexed : Features.Prominence.DefinitenessLevel → Bool

  Which definiteness levels trigger indexing

def Aissen2003.IndexingFragment.mk' (name iso639 family : String) (role : Features.Prominence.ArgumentRole) (personIndexed : IndexingPersonLevel → Bool) (animacyIndexed : Features.Prominence.AnimacyLevel → Bool) (definitenessIndexed : Features.Prominence.DefinitenessLevel → Bool) : IndexingFragment

Smart constructor for IndexingFragment. Computes the 2D marks predicate as the product of animacyIndexed and definitenessIndexed, and sets channel :=.indexing.

Equations

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

def Aissen2003.IndexingFragment.personConditioned (f : IndexingFragment) : Bool

A dimension is conditioning if the marking predicate is non-uniform: some levels are indexed and some are not.

Equations

• f.personConditioned = (Aissen2003.IndexingPersonLevel.all.any f.personIndexed && !Aissen2003.IndexingPersonLevel.all.all f.personIndexed)

def Aissen2003.IndexingFragment.animacyConditioned (f : IndexingFragment) : Bool

Equations

• f.animacyConditioned = (Features.Prominence.AnimacyLevel.all.any f.animacyIndexed && !Features.Prominence.AnimacyLevel.all.all f.animacyIndexed)

def Aissen2003.IndexingFragment.definitenessConditioned (f : IndexingFragment) : Bool

Equations

• f.definitenessConditioned = (Features.Prominence.DefinitenessLevel.all.any f.definitenessIndexed && !Features.Prominence.DefinitenessLevel.all.all f.definitenessIndexed)

def Aissen2003.IndexingFragment.isDifferential (f : IndexingFragment) : Bool

At least one dimension conditions the indexing (i.e., is non-uniform).

Equations

• f.isDifferential = (f.personConditioned || f.animacyConditioned || f.definitenessConditioned)

def Aissen2003.IndexingFragment.pPolarityCorrect (f : IndexingFragment) : Bool

P indexing has correct polarity if it targets the PROMINENT end: SAP over 3rd, human over inanimate, definite over nonspecific.

Equations

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

def Aissen2003.IndexingFragment.aPolarityCorrect (f : IndexingFragment) : Bool

A indexing has correct polarity if it targets the NON-PROMINENT end: 3rd over SAP, inanimate over human, nonspecific over definite.

Equations

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

def Aissen2003.IndexingFragment.polarityCorrect (f : IndexingFragment) : Bool

Role-appropriate polarity check. T behaves like P (targets prominent), R behaves like A (targets non-prominent). S is vacuously correct.

Equations

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

Languages where the P argument is differentially indexed. Prominent Ps (SAP, human, definite) are MORE likely to be indexed.

Marking predicates encode the actual pattern per scale. For scales that
are not conditioning, the predicate is uniformly `true` (all levels
indexed). For conditioning scales, the predicate marks the prominent
end as `true` and the non-prominent end as `false`.

Source references are from [just-2024]. 

def Aissen2003.abkhaz : IndexingFragment

Abkhaz (NW Caucasian): P indexed only for SAP.

Equations

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

def Aissen2003.amharic : IndexingFragment

Amharic (Semitic): P indexed for SAP and definite objects.

Equations

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

def Aissen2003.basque : IndexingFragment

Basque (Isolate): object agreement only for SAP objects.

Equations

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

def Aissen2003.georgian : IndexingFragment

Georgian (Kartvelian): P agreement conditioned by person — indirect objects (dative) are indexed for SAP only.

Equations

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

def Aissen2003.hungarian : IndexingFragment

Hungarian (Uralic): definite conjugation triggered by definite objects; indefinite conjugation for indefinite objects. See also Hungarian.Predicates for the conjugation split.

Equations

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

def Aissen2003.kagulu : IndexingFragment

Kagulu (Bantu): object marker for animate+ objects.

Equations

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

def Aissen2003.kinzadi : IndexingFragment

KiNzadi (Bantu): P indexed for SAP only.

Equations

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

def Aissen2003.koorete : IndexingFragment

Koorete (Omotic): P indexed for SAP only.

Equations

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

def Aissen2003.maltese : IndexingFragment

Maltese (Semitic): definite object agreement — verb agrees with definite objects via suffixed object markers (Just & Čéplö 2022).

Equations

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

def Aissen2003.nkoreKiga : IndexingFragment

Nkore-Kiga (Bantu): object marker for SAP objects.

Equations

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

def Aissen2003.romanian : IndexingFragment

Romanian (Romance): clitic doubling conditioned by person, animacy, and definiteness. SAP + human + definite = doubled.

Equations

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

def Aissen2003.somali : IndexingFragment

Somali (Cushitic): P indexed for SAP — full paradigm for SAP objects, reduced for 3rd person. Focus/topicality also plays a role but is not captured in the prominence grid.

Equations

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

def Aissen2003.swahili : IndexingFragment

Swahili (Bantu): object marker obligatory for human objects, optional/ absent for non-human.

Equations

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

def Aissen2003.teiwa : IndexingFragment

Teiwa (Trans-New Guinea): P indexed for animate objects.

Equations

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

def Aissen2003.welsh : IndexingFragment

Welsh (Celtic): synthetic agreement only with pronominal (SAP) objects; analytic (no agreement) with 3rd person full NPs.

Equations

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

def Aissen2003.zulu : IndexingFragment

Zulu (Bantu): object marker for animate objects.

Equations

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

def Aissen2003.spokenArabic : IndexingFragment

Spoken Arabic varieties (Semitic): P indexed for SAP only — object suffixes restricted to pronominal objects.

Equations

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

Languages where the A argument is differentially indexed. Non-prominent As (3rd person, inanimate, indefinite) are MORE likely to be indexed. The polarity is REVERSED relative to P indexing.

Source references from [just-2024]. 

def Aissen2003.jamsay : IndexingFragment

Jamsay (Dogon): A indexed only for 3rd person agents — SAP agents are not cross-referenced on the verb.

Equations

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

def Aissen2003.kharia : IndexingFragment

Kharia (Munda): A indexed for 3rd person agents.

Equations

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

def Aissen2003.mundari : IndexingFragment

Mundari (Munda): A indexed for 3rd person agents.

Equations

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

def Aissen2003.juang : IndexingFragment

Juang (Munda): A indexed for 3rd person agents.

Equations

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

def Aissen2003.anywa : IndexingFragment

Anywa (Nilotic): A indexed for 3rd person agents only — SAP agents are not cross-referenced.

Equations

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

def Aissen2003.reyesano : IndexingFragment

Reyesano (Tacanan): A indexed for 3rd person and non-human agents.

Equations

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

def Aissen2003.easternMansi : IndexingFragment

Eastern Mansi (Uralic): A indexed for indefinite/non-topical agents.

Equations

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

def Aissen2003.pIndexingLanguages : List IndexingFragment

All differential P indexing languages in the sample.

Equations

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

def Aissen2003.aIndexingLanguages : List IndexingFragment

All differential A indexing languages in the sample.

Equations

• Aissen2003.aIndexingLanguages = [Aissen2003.jamsay, Aissen2003.kharia, Aissen2003.mundari, Aissen2003.juang, Aissen2003.anywa, Aissen2003.reyesano, Aissen2003.easternMansi]

def Aissen2003.allIndexingLanguages : List IndexingFragment

All differential indexing languages.

Equations

• Aissen2003.allIndexingLanguages = Aissen2003.pIndexingLanguages ++ Aissen2003.aIndexingLanguages

theorem Aissen2003.pIndexing_all_roleP : (pIndexingLanguages.all fun (x : IndexingFragment) => x.role == Features.Prominence.ArgumentRole.P) = true

All P indexing languages have role P.

theorem Aissen2003.aIndexing_all_roleA : (aIndexingLanguages.all fun (x : IndexingFragment) => x.role == Features.Prominence.ArgumentRole.A) = true

All A indexing languages have role A.

theorem Aissen2003.all_differential : (allIndexingLanguages.all fun (x : IndexingFragment) => x.isDifferential) = true

All profiles are genuinely differential (at least one conditioning factor is non-uniform). Derived from the marking predicates.

The collections below are COMPUTED from the marking predicates via personConditioned, animacyConditioned, definitenessConditioned — if a language's marking predicate changes, they update automatically.

def Aissen2003.pPersonConditioned : List IndexingFragment

P indexing languages conditioned by person (derived).

Equations

• Aissen2003.pPersonConditioned = List.filter (fun (x : Aissen2003.IndexingFragment) => x.personConditioned) Aissen2003.pIndexingLanguages

def Aissen2003.pAnimacyConditioned : List IndexingFragment

P indexing languages conditioned by animacy (derived).

Equations

• Aissen2003.pAnimacyConditioned = List.filter (fun (x : Aissen2003.IndexingFragment) => x.animacyConditioned) Aissen2003.pIndexingLanguages

def Aissen2003.pDefinitenessConditioned : List IndexingFragment

P indexing languages conditioned by definiteness (derived).

Equations

• Aissen2003.pDefinitenessConditioned = List.filter (fun (x : Aissen2003.IndexingFragment) => x.definitenessConditioned) Aissen2003.pIndexingLanguages

def Aissen2003.aPersonConditioned : List IndexingFragment

A indexing languages conditioned by person (derived).

Equations

• Aissen2003.aPersonConditioned = List.filter (fun (x : Aissen2003.IndexingFragment) => x.personConditioned) Aissen2003.aIndexingLanguages

theorem Aissen2003.person_dominates_P : pPersonConditioned.length > pAnimacyConditioned.length ∧ pPersonConditioned.length > pDefinitenessConditioned.length

Person is the most common conditioning factor for P indexing: more P-indexing languages are person-conditioned than animacy- or definiteness-conditioned.

theorem Aissen2003.person_dominates_A : aPersonConditioned.length > (List.filter (fun (x : IndexingFragment) => x.animacyConditioned) aIndexingLanguages).length ∧ aPersonConditioned.length > (List.filter (fun (x : IndexingFragment) => x.definitenessConditioned) aIndexingLanguages).length

Person is the most common conditioning factor for A indexing: more A-indexing languages are person-conditioned than animacy- or definiteness-conditioned.

"The very same referential properties condition both differential P and differential A indexing."

theorem Aissen2003.person_conditions_both : ((pIndexingLanguages.any fun (x : IndexingFragment) => x.personConditioned) && decide ((aIndexingLanguages.any fun (x : IndexingFragment) => x.personConditioned) = true)) = true

Person conditions both P and A indexing.

theorem Aissen2003.animacy_conditions_both : ((pIndexingLanguages.any fun (x : IndexingFragment) => x.animacyConditioned) && decide ((aIndexingLanguages.any fun (x : IndexingFragment) => x.animacyConditioned) = true)) = true

Animacy conditions both P and A indexing.

theorem Aissen2003.definiteness_conditions_both : ((pIndexingLanguages.any fun (x : IndexingFragment) => x.definitenessConditioned) && decide ((aIndexingLanguages.any fun (x : IndexingFragment) => x.definitenessConditioned) = true)) = true

Definiteness conditions both P and A indexing.

"The directions in which these scales operate form a mirror image: indexing targets prominent P arguments on the one hand and non-prominent A arguments on the other."

theorem Aissen2003.p_indexing_targets_prominent : (pIndexingLanguages.all fun (x : IndexingFragment) => x.pPolarityCorrect) = true

All P indexing languages have correct polarity: they target the prominent end of each conditioning scale.

theorem Aissen2003.a_indexing_targets_nonprominent : (aIndexingLanguages.all fun (x : IndexingFragment) => x.aPolarityCorrect) = true

All A indexing languages have correct polarity: they target the non-prominent end of each conditioning scale.

theorem Aissen2003.mirror_image_universal : (allIndexingLanguages.all fun (x : IndexingFragment) => x.polarityCorrect) = true

The mirror image holds universally across the sample: every language has role-appropriate polarity.

For languages where animacy and/or definiteness condition indexing, we verify monotonicity of the inherited DifferentialMarkingProfile on the 2D grid. The marks predicate is derived from the fragment's animacyIndexed and definitenessIndexed — no separate stipulation.

theorem Aissen2003.hungarian_monotone : hungarian.isMonotone = true

All animacy/definiteness-conditioned profiles are monotone.

theorem Aissen2003.swahili_monotone : swahili.isMonotone = true

theorem Aissen2003.kagulu_monotone : kagulu.isMonotone = true

theorem Aissen2003.easternMansi_monotone : easternMansi.isMonotone = true

theorem Aissen2003.swahili_animacy_only : swahili.isAnimacyOnly = true

Swahili P indexing depends only on animacy (definiteness is irrelevant).

theorem Aissen2003.kagulu_animacy_only : kagulu.isAnimacyOnly = true

Kagulu P indexing depends only on animacy.

theorem Aissen2003.hungarian_definiteness_only : hungarian.isDefinitenessOnly = true

Hungarian P indexing depends only on definiteness (animacy is irrelevant).

theorem Aissen2003.easternMansi_definiteness_only : easternMansi.isDefinitenessOnly = true

Eastern Mansi A indexing depends only on definiteness.

theorem Aissen2003.bantu_all_P : (allIndexingLanguages.all fun (p : IndexingFragment) => if (p.family == "Bantu") = true then p.role == Features.Prominence.ArgumentRole.P else true) = true

Bantu languages in the sample all show P indexing.

theorem Aissen2003.munda_all_A : (allIndexingLanguages.all fun (p : IndexingFragment) => if (p.family == "Austroasiatic (Munda)") = true then p.role == Features.Prominence.ArgumentRole.A else true) = true

Munda languages in the sample all show A indexing.

"Prominent arguments, be it A or P (or probably any other role), tend to be indexed more readily than arguments which are low in identifiability, animacy or topicality."

The mirror image is NOT a coincidence — it follows from a single
principle (indexing tracks prominent referents) combined with different
default prominence per role (A defaults high, P defaults low). 

theorem Aissen2003.prominent_P_indexed : (pPersonConditioned.all fun (x : IndexingFragment) => x.personIndexed IndexingPersonLevel.sap) = true

For every person-conditioned P-indexing language, SAP is indexed (= prominent P gets indexed).

theorem Aissen2003.nonprominent_A_indexed : (aPersonConditioned.all fun (x : IndexingFragment) => x.personIndexed IndexingPersonLevel.third) = true

For every person-conditioned A-indexing language, 3rd person is indexed (= non-prominent A gets indexed, because A's default is prominent).

theorem Aissen2003.complement_differs_by_role : (pPersonConditioned.all fun (f : IndexingFragment) => !f.personIndexed IndexingPersonLevel.third) = true ∧ (aPersonConditioned.all fun (f : IndexingFragment) => !f.personIndexed IndexingPersonLevel.sap) = true

The unified principle predicts that the COMPLEMENT of "indexed" differs by role: P-indexing excludes 3rd person, A-indexing excludes SAP. Both follow from "index the prominent referent" + role defaults.

DOMProfile is an abbreviation for DifferentialMarkingProfile (specialized to role P + channel flagging), and IndexingFragment extends DifferentialMarkingProfile (with channel = .indexing). Both DOM profiles and indexing fragments inherit all DMP infrastructure (monotonicity, dimensionality, cutoff constructors, mirror image) directly — no conversion or bridge theorems needed.

Just's binary person split (SAP vs 3rd) is exactly Preminger's [±participant] feature decomposition.

def Aissen2003.personToLevel : Person → IndexingPersonLevel

Map a Person to Just's IndexingPersonLevel. 1st/2nd → SAP, 3rd → third.

Equations

• Aissen2003.personToLevel Person.first = Aissen2003.IndexingPersonLevel.sap
• Aissen2003.personToLevel Person.firstInclusive = Aissen2003.IndexingPersonLevel.sap
• Aissen2003.personToLevel Person.firstExclusive = Aissen2003.IndexingPersonLevel.sap
• Aissen2003.personToLevel Person.second = Aissen2003.IndexingPersonLevel.sap
• Aissen2003.personToLevel Person.third = Aissen2003.IndexingPersonLevel.third
• Aissen2003.personToLevel Person.zero = Aissen2003.IndexingPersonLevel.third

theorem Aissen2003.personLevel_matches_participant : (personToLevel Person.first == IndexingPersonLevel.sap) = (Minimalist.decomposePerson Person.first).hasParticipant ∧ (personToLevel Person.second == IndexingPersonLevel.sap) = (Minimalist.decomposePerson Person.second).hasParticipant ∧ (personToLevel Person.third == IndexingPersonLevel.sap) = (Minimalist.decomposePerson Person.third).hasParticipant

personToLevel agrees with decomposePerson on the participant split: SAP ↔ [+participant], third ↔ [−participant].

theorem Aissen2003.personLevel_rank_matches_probe_rank : IndexingPersonLevel.sap.rank > IndexingPersonLevel.third.rank ∧ Minimalist.probeResolutionRank Person.first false > Minimalist.probeResolutionRank Person.third false ∧ Minimalist.probeResolutionRank Person.second false > Minimalist.probeResolutionRank Person.third false

SAP has higher prominence rank than 3rd, just as [+participant] gives higher probe resolution rank.

Kaqchikel indexes both A and P arguments uniformly across all person-number combinations. This is a NON-differential system: there is no prominence-based asymmetry in which arguments get indexed.

[just-2024] defines differential indexing against this kind of
baseline: a differential system is one where indexing depends on
prominence properties. 

theorem Aissen2003.kaqchikel_indexes_all (p : Kaqchikel.ArgPosition) (h : p ∈ Kaqchikel.kaqArgPositions) : p.IsPhiAgreed

Kaqchikel indexes all three argument positions (agent, patient, intranS). This makes it non-differential: no prominence condition gates indexing.

theorem Aissen2003.kaqchikel_A_and_P_indexed : Kaqchikel.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.A ∧ Kaqchikel.ArgPosition.IsPhiAgreed Features.Prominence.ArgumentRole.P

Both A (agent) and P (patient) are indexed in Kaqchikel: agent via Set A on Voice/v, patient via Set B on Infl/T.

theorem Aissen2003.kaqchikel_dual_paradigms : Agreement.Paradigm.realize Kaqchikel.setAExponent (Agreement.Cell.pn UD.Person.first UD.Number.Sing) ≠ Agreement.Paradigm.realize Kaqchikel.setBExponent (Agreement.Cell.pn UD.Person.first UD.Number.Sing) ∧ Agreement.Paradigm.realize Kaqchikel.setAExponent (Agreement.Cell.pn UD.Person.second UD.Number.Sing) ≠ Agreement.Paradigm.realize Kaqchikel.setBExponent (Agreement.Cell.pn UD.Person.second UD.Number.Sing)

The A marker paradigm (Set A) and P marker paradigm (Set B) are distinct: every person-number combination gets a unique marker in each set (except 3SG which is ∅ in Set B).

def Aissen2003.kaqArgToRole : Kaqchikel.ArgPosition → Features.Prominence.ArgumentRole

Map Kaqchikel argument positions to Just's A/P roles. The absolutive collapse: S patterns with P, A stays distinct; ditransitive R/T default to P (consistent with absolutive grouping).

Equations

• Aissen2003.kaqArgToRole Features.Prominence.ArgumentRole.A = Features.Prominence.ArgumentRole.A
• Aissen2003.kaqArgToRole Features.Prominence.ArgumentRole.S = Features.Prominence.ArgumentRole.P
• Aissen2003.kaqArgToRole Features.Prominence.ArgumentRole.P = Features.Prominence.ArgumentRole.P
• Aissen2003.kaqArgToRole Features.Prominence.ArgumentRole.R = Features.Prominence.ArgumentRole.P
• Aissen2003.kaqArgToRole Features.Prominence.ArgumentRole.T = Features.Prominence.ArgumentRole.P

theorem Aissen2003.kaqArg_role_mapping : kaqArgToRole Features.Prominence.ArgumentRole.A = Features.Prominence.ArgumentRole.A ∧ kaqArgToRole Features.Prominence.ArgumentRole.P = Features.Prominence.ArgumentRole.P ∧ kaqArgToRole Features.Prominence.ArgumentRole.S = Features.Prominence.ArgumentRole.P

Identity on A and P; the load-bearing structure is the S → P collapse encoded in kaqArgToRole.

theorem Aissen2003.erg_abs_matches_AP : Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.A ≠ Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.P ∧ Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.P = Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.S

Ergative-absolutive alignment: A is distinguished (ERG) while P and S pattern together (ABS). This parallels Just's A/P split.

Person is the dominant conditioning factor for both P indexing and A indexing (§10). The structural correlate is that the [participant] probe (π⁰) takes priority over the [plural] probe (#⁰) under the two-probe relativized-probing system [BR03] — NOT a salience hierarchy. [Pre14] Ch. 7 explicitly argues against direct salience-scale primitives; the rank ordering below is a surface effect of probe priority, not a hierarchy-as-grammatical-primitive. See Studies/Preminger2014.lean for the anti-hierarchy theorems.

theorem Aissen2003.two_probe_surface_ranking : Minimalist.probeResolutionRank Person.first false > Minimalist.probeResolutionRank Person.third true ∧ Minimalist.probeResolutionRank Person.third true > Minimalist.probeResolutionRank Person.third false

Two-probe surface ranking [BR03]: [+participant] cells outrank [+plural,−participant] cells, which outrank 3SG. The typological frequency hierarchy (person > animacy > definiteness) parallels this — person features are both structurally privileged at the probe level and typologically dominant in indexing systems.

The Basque agreement fragment (Basque.Agreement) encodes the same person-conditioned P indexing that [Jus24] reports. We prove that the Fragment's pIsIndexed matches the survey data.

theorem Aissen2003.basque_fragment_matches_survey : Basque.Agreement.pIsIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = basque.personIndexed IndexingPersonLevel.sap ∧ Basque.Agreement.pIsIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = basque.personIndexed IndexingPersonLevel.sap ∧ Basque.Agreement.pIsIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = basque.personIndexed IndexingPersonLevel.third

Basque Fragment's P indexing matches the Just survey: SAP → indexed, 3rd → not indexed, exactly as basque.personIndexed.

theorem Aissen2003.basque_fragment_is_differential : Agreement.Cell.pnCells.any Basque.Agreement.pIsIndexed = true ∧ (!decide (Agreement.Cell.pnCells.all Basque.Agreement.pIsIndexed = true)) = true

Basque Fragment confirms differential P indexing: some indexed, some not.

The Georgian agreement fragment (Georgian.Agreement) derives P indexing from the presence of object agreement prefixes (m-, g-, gv-). The indexed/not-indexed split aligns with SAP vs 3rd — same as the Just survey data.

theorem Aissen2003.georgian_fragment_matches_survey : Georgian.Agreement.isIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = georgian.personIndexed IndexingPersonLevel.sap ∧ Georgian.Agreement.isIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = georgian.personIndexed IndexingPersonLevel.sap ∧ Georgian.Agreement.isIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = georgian.personIndexed IndexingPersonLevel.third

Georgian Fragment's P indexing matches the Just survey.

theorem Aissen2003.georgian_indexing_grounded : (Agreement.Cell.pnCells.all fun (c : Agreement.Cell) => Georgian.Agreement.isIndexed c == (Georgian.Agreement.objectAgr.realize c).isSome) = true

Georgian Fragment's P indexing is grounded in object prefix morphology: indexed iff the object paradigm realizes the cell. Not stipulated — follows from the data.

The Hungarian predicate fragment (Hungarian.Predicates) models the definite/indefinite conjugation split. This IS Just's differential P indexing by definiteness: the verb's agreement paradigm changes depending on whether the object is definite.

The fragment's `formPastDef ≠ formPastIndef` encodes the same claim
as the Just survey entry `hungarian.definitenessConditioned`. 

theorem Aissen2003.hungarian_conjugation_split : Hungarian.Predicates.tud.formPastDef ≠ Hungarian.Predicates.tud.formPastIndef ∧ Hungarian.Predicates.mond.formPastDef ≠ Hungarian.Predicates.mond.formPastIndef ∧ Hungarian.Predicates.hisz.formPastDef ≠ Hungarian.Predicates.hisz.formPastIndef

Hungarian verbs have distinct definite vs indefinite conjugation forms. This IS the morphological reflex of differential P indexing by definiteness.

theorem Aissen2003.hungarian_definiteness_conditioned : hungarian.definitenessConditioned = true

Hungarian is definiteness-conditioned (derived from the marking predicate), confirming the Fragment's conjugation split.

theorem Aissen2003.hungarian_not_person_conditioned : hungarian.personConditioned = false

Hungarian is NOT person-conditioned — all persons can trigger both conjugation types.