Just 2024: Differential A and P Indexing

[just-2024] [aissen-2003] [haspelmath-2019] [siewierska-2004] [preminger-2014] [haspelmath-2021]

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

Flagging = case morphology on the NP; indexing = verbal agreement/cross-referencing ([haspelmath-2019], 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, carrying a Features.Prominence.MarkingPattern grid
• 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 [preminger-2014]'s [±participant]
• basque_fragment_matches_survey, georgian_fragment_matches_survey, hungarian_conjugation_split: fragment paradigms ground the survey rows

inductive Just2024.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 [preminger-2014]'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

@[instance_reducible]

instance Just2024.instDecidableEqIndexingPersonLevel : DecidableEq IndexingPersonLevel

Equations

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

@[instance_reducible]

instance Just2024.instReprIndexingPersonLevel : Repr IndexingPersonLevel

Equations

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

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

Equations

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

@[instance_reducible]

instance Just2024.instInhabitedIndexingPersonLevel : Inhabited IndexingPersonLevel

Equations

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

def Just2024.IndexingPersonLevel.rank : IndexingPersonLevel → ℕ

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

Equations

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

def Just2024.IndexingPersonLevel.all : List IndexingPersonLevel

All indexing person levels.

Equations

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

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

structure Just2024.IndexingFragment : Type

A differential indexing fragment for a single language: language metadata, the indexed argument role, and per-dimension marking predicates.

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

  Language name

• iso639 : String

  ISO 639-3 code

• family : String

  Language family

• role : ArgumentRole

  Which argument role is differentially indexed

• 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 Just2024.IndexingFragment.mk' (name iso639 family : String) (role : ArgumentRole) (personIndexed : IndexingPersonLevel → Bool) (animacyIndexed : Features.Prominence.AnimacyLevel → Bool) (definitenessIndexed : Features.Prominence.DefinitenessLevel → Bool) : IndexingFragment

Positional constructor for IndexingFragment.

Equations

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

def Just2024.IndexingFragment.marks (f : IndexingFragment) : Features.Prominence.MarkingPattern

The fragment's animacy × definiteness marking grid: the product of animacyIndexed and definitenessIndexed.

Equations

• f.marks a d = (f.animacyIndexed a && f.definitenessIndexed d)

def Just2024.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 = (Just2024.IndexingPersonLevel.all.any f.personIndexed && !Just2024.IndexingPersonLevel.all.all f.personIndexed)

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

Equations

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

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

Equations

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

def Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.abkhaz : IndexingFragment

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

Equations

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

def Just2024.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 Just2024.basque : IndexingFragment

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

Equations

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

def Just2024.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 Just2024.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 Just2024.kagulu : IndexingFragment

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

Equations

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

def Just2024.kinzadi : IndexingFragment

KiNzadi (Bantu): P indexed for SAP only.

Equations

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

def Just2024.koorete : IndexingFragment

Koorete (Omotic): P indexed for SAP only.

Equations

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

def Just2024.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 Just2024.nkoreKiga : IndexingFragment

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

Equations

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

def Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.zulu : IndexingFragment

Zulu (Bantu): object marker for animate objects.

Equations

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

def Just2024.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 Just2024.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 Just2024.kharia : IndexingFragment

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

Equations

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

def Just2024.mundari : IndexingFragment

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

Equations

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

def Just2024.juang : IndexingFragment

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

Equations

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

def Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.aIndexingLanguages : List IndexingFragment

All differential A indexing languages in the sample.

Equations

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

def Just2024.allIndexingLanguages : List IndexingFragment

All differential indexing languages.

Equations

• Just2024.allIndexingLanguages = Just2024.pIndexingLanguages ++ Just2024.aIndexingLanguages

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

All P indexing languages have role P.

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

All A indexing languages have role A.

theorem Just2024.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 Just2024.pPersonConditioned : List IndexingFragment

P indexing languages conditioned by person (derived).

Equations

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

def Just2024.pAnimacyConditioned : List IndexingFragment

P indexing languages conditioned by animacy (derived).

Equations

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

def Just2024.pDefinitenessConditioned : List IndexingFragment

P indexing languages conditioned by definiteness (derived).

Equations

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

def Just2024.aPersonConditioned : List IndexingFragment

A indexing languages conditioned by person (derived).

Equations

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

theorem Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.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, monotonicity of the role-appropriate direction holds on the 2D grid: upper set for the P-indexing languages, lower set for A-indexing Eastern Mansi. The marks grid is derived from the fragment's animacyIndexed and definitenessIndexed — no separate stipulation.

theorem Just2024.hungarian_monotone : hungarian.marks.MonotoneP

All animacy/definiteness-conditioned patterns are monotone.

theorem Just2024.swahili_monotone : swahili.marks.MonotoneP

theorem Just2024.kagulu_monotone : kagulu.marks.MonotoneP

theorem Just2024.easternMansi_monotone : easternMansi.marks.MonotoneA

theorem Just2024.swahili_animacy_only : swahili.marks.AnimacyOnly

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

theorem Just2024.kagulu_animacy_only : kagulu.marks.AnimacyOnly

Kagulu P indexing depends only on animacy.

theorem Just2024.hungarian_definiteness_only : hungarian.marks.DefinitenessOnly

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

theorem Just2024.easternMansi_definiteness_only : easternMansi.marks.DefinitenessOnly

Eastern Mansi A indexing depends only on definiteness.

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

Bantu languages in the sample all show P indexing.

theorem Just2024.munda_all_A : (allIndexingLanguages.all fun (p : IndexingFragment) => if (p.family == "Austroasiatic (Munda)") = true then p.role == 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 Just2024.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 Just2024.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 Just2024.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.

[aissen-2003]'s DOM grids and IndexingFragment.marks are both Features.Prominence.MarkingPatterns, so flagging and indexing share the monotonicity, dimensionality, and cutoff infrastructure directly — no conversion or bridge theorems needed.

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

def Just2024.personToLevel : Person → IndexingPersonLevel

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

Equations

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

theorem Just2024.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 Just2024.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 Just2024.kaqchikel_indexes_all (p : ArgumentRole) (h : p ∈ ArgumentRole.core) : Kaqchikel.IsPhiAgreed p

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

theorem Just2024.kaqchikel_A_and_P_indexed : Kaqchikel.IsPhiAgreed ArgumentRole.A ∧ Kaqchikel.IsPhiAgreed 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 Just2024.kaqchikel_dual_paradigms : Agreement.Paradigm.realize (Kaqchikel.setAExponent Phonology.Segment.Class.consonant) (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 Phonology.Segment.Class.consonant) (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 Just2024.kaqArgToRole : ArgumentRole → ArgumentRole

The absolutive collapse on coding roles: S patterns with P, A stays distinct; ditransitive R/T default to P (consistent with absolutive grouping).

Equations

• Just2024.kaqArgToRole ArgumentRole.A = ArgumentRole.A
• Just2024.kaqArgToRole ArgumentRole.S = ArgumentRole.P
• Just2024.kaqArgToRole ArgumentRole.P = ArgumentRole.P
• Just2024.kaqArgToRole ArgumentRole.R = ArgumentRole.P
• Just2024.kaqArgToRole ArgumentRole.T = ArgumentRole.P

theorem Just2024.kaqArg_role_mapping : kaqArgToRole ArgumentRole.A = ArgumentRole.A ∧ kaqArgToRole ArgumentRole.P = ArgumentRole.P ∧ kaqArgToRole ArgumentRole.S = ArgumentRole.P

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

theorem Just2024.erg_abs_matches_AP : Mayan.caseKaqchikel UD.Aspect.Perf ArgumentRole.A ≠ Mayan.caseKaqchikel UD.Aspect.Perf ArgumentRole.P ∧ Mayan.caseKaqchikel UD.Aspect.Perf ArgumentRole.P = Mayan.caseKaqchikel UD.Aspect.Perf 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 [bejar-rezac-2003] — NOT a salience hierarchy. [preminger-2014] 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 Just2024.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 [bejar-rezac-2003]: [+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 [just-2024] reports. We prove that the Fragment's pIsIndexed matches the survey data.

theorem Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.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 Just2024.hungarian_definiteness_conditioned : hungarian.definitenessConditioned = true

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

theorem Just2024.hungarian_not_person_conditioned : hungarian.personConditioned = false

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