Shared Pronoun and Allocutive Entry Types

@cite{alok-bhalla-2026}

Cross-linguistic structures for pronoun inventories and allocutive markers, shared across all Fragment/*/Pronouns.lean files.

PronounEntry

Covers the union of fields needed by all language fragments:

• Core: form, person, number (all fragments)
• Morphosyntactic: case_ (Galician, English)
• Sociolinguistic: register (all SA-based fragments)
• Orthographic: script (Korean hangul, Japanese kanji)

AllocutiveEntry

Shared structure for allocutive markers — verbal suffixes (Hindi, Magahi, Maithili, Punjabi, Tamil, Basque), particles (Korean, Japanese), or clitics (Galician) that realize speaker-addressee agreement.

structure Core.Pronouns.PronounEntry : Type

Cross-linguistic pronoun entry.

Covers personal pronouns across all Fragment languages. Language-specific extensions (e.g., English PronounType/wh) remain in their respective Fragment files.

• form : String

  Surface form (romanization or orthographic)

• person : Option Person

  Grammatical person (UD.Person)

• number : Option Number

  Grammatical number (UD.Number)

• case_ : Option Case

  Grammatical case (UD.Case)

• register : Register.Level

  Register level (formality/honorifics). Binary T/V systems use .informal/.formal; ternary honorific systems (Hindi, Magahi, Maithili, Korean) use all three levels.

• referentialPerson : Option Prominence.PersonLevel

  Referential person — who the pronoun refers to in terms of discourse role — when it diverges from formal/agreement person. For polite pronouns (Italian LEI, Spanish USTED, German SIE), the formal person field is 3rd (governing agreement, clitic allomorphy, reflexive binding), while referentialPerson is 2nd (governing the PCC, Fancy Constraint, resolved agreement). For ordinary pronouns, leave as none — referential person coincides with formal person. @cite{adamson-zompi-2025}

• script : Option String

  Native script form (hangul, kanji, Devanagari, etc.)

def Core.Pronouns.instReprPronounEntry.repr : PronounEntry → ℕ → Std.Format

Equations

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

instance Core.Pronouns.instReprPronounEntry : Repr PronounEntry

Equations

• Core.Pronouns.instReprPronounEntry = { reprPrec := Core.Pronouns.instReprPronounEntry.repr }

instance Core.Pronouns.instBEqPronounEntry : BEq PronounEntry

Equations

• Core.Pronouns.instBEqPronounEntry = { beq := Core.Pronouns.instBEqPronounEntry.beq }

def Core.Pronouns.instBEqPronounEntry.beq : PronounEntry → PronounEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.Pronouns.instBEqPronounEntry.beq x✝¹ x✝ = false

structure Core.Pronouns.AllocutiveEntry : Type

Cross-linguistic allocutive marker entry.

Covers verbal suffixes, particles, and clitics that realize allocutive agreement across all Fragment languages.

• form : String

  Surface form of the marker

• register : Register.Level

  Register level (matching PronounEntry.register scale)

• gloss : String

  Gloss string (e.g., "IMP.NH", "POL", "2sg.DAT.fam")

instance Core.Pronouns.instReprAllocutiveEntry : Repr AllocutiveEntry

Equations

• Core.Pronouns.instReprAllocutiveEntry = { reprPrec := Core.Pronouns.instReprAllocutiveEntry.repr }

def Core.Pronouns.instReprAllocutiveEntry.repr : AllocutiveEntry → ℕ → Std.Format

Equations

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

instance Core.Pronouns.instBEqAllocutiveEntry : BEq AllocutiveEntry

Equations

• Core.Pronouns.instBEqAllocutiveEntry = { beq := Core.Pronouns.instBEqAllocutiveEntry.beq }

def Core.Pronouns.instBEqAllocutiveEntry.beq : AllocutiveEntry → AllocutiveEntry → Bool

Equations

• Core.Pronouns.instBEqAllocutiveEntry.beq { form := a, register := a_1, gloss := a_2 } { form := b, register := b_1, gloss := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Core.Pronouns.instBEqAllocutiveEntry.beq x✝¹ x✝ = false