Pronoun capabilities — a mixin tower over pronoun carriers

Pronoun entries (Pronoun, PersonalPronoun, IndefinitePronoun, …) are bundled structure values — many per language, like mathlib's MonoidHom. This file gives the capabilities a carrier α can have, as typeclass mixins abstracting over the representation — the MonoidHomClass/ContinuousMul-over-MonoidHom/Mul relationship, applied to pronouns. A consumer (binding engine, agreement module, …) then requires exactly the axes it touches: [Proform α] for form/φ, [Bound α] for the Principle A/B/C role, and so on — composed by instance parameters with no extends-diamond. The carrier may be a record (Pronoun), a syntactic object (Word), or a future theory representation; each supplies its own instances.

Main declarations

• Proform — the spine: a carrier exposes a surface form and agreement phi-features.
• instance Bound Pronoun / Bound PersonalPronoun — the pronoun carriers' binding-axis instances. The Bound class (with Anaphoric/Pronominal/Referring and the Bound.Is* element predicates) is theory-neutral and lives beside its partial companion Features.BindingSource in Features/CoreferenceStatus.lean.
• bindingClassOf_toWord — the faithfulness certificate: the binding engine's canonical morphology source (Binding.bindingClassOf) agrees with the Bound mixin on every projected pro-form, so the surface engine and the carrier capability never diverge.
• Deictic — orthogonal data-mixin (register / referential person).

Implementation notes

Capabilities live near their domain (mathlib-style: ContinuousMul is in Topology, not Algebra). The word-class-neutral Indefinite capability ([Indefinite α], Haspelmath function-coverage) therefore lives in Features/Indefinite.lean, and the binding axis Bound lives in Features/CoreferenceStatus.lean — neither is pronoun-specific. Two further axes are deferred, each for a principled reason. Deficiency ([CS99a] Pronoun.Strength) is per-series, not per-element: every carrier's strength is carrier-uniform (Italian clitics are all .clitic; the Mixtec clitic/nonclitic fields have fixed strengths), so an α → Strength accessor would be constant on every carrier — a per-type fact, not a per-element capability. It is served by the Pronoun.strength field (series-level, none when not homogeneous) and the Strength linear order, not by a class. The finer lexical-kind axis (personal vs relative vs interrogative vs demonstrative) is Pronoun.pronType — real UD morphology on the carrier (no invented enum), threaded onto the projected word by toWord.

The spine: Proform

class Proform (α : Type u_1) : Type u_1

A pronoun-like carrier exposes a surface form and agreement phi-features — everything true of every pronoun, the base every other capability builds over (cf. Mul/Semigroup as the base operation class).

• form : α → String

  Surface form (romanization or orthographic).

• phi : α → UD.MorphFeatures

  Agreement φ-features (person/number/gender).

@[implicit_reducible]

instance instProformWord : Proform Word

Equations

• instProformWord = { form := Word.form, phi := Word.phi }

@[implicit_reducible]

instance instProformPronoun : Proform Pronoun

Equations

• instProformPronoun = { form := Pronoun.form, phi := fun (p : Pronoun) => p.toWord.phi }

@[implicit_reducible]

instance instProformPersonalPronoun : Proform PersonalPronoun

Equations

• instProformPersonalPronoun = { form := fun (p : PersonalPronoun) => p.form, phi := fun (p : PersonalPronoun) => p.toWord.phi }

The pronoun carriers' Bound instances, and the faithfulness certificate

@[implicit_reducible]

instance instBoundPronoun : Bound Pronoun

A bare Pronoun's declared class, defaulting an undeclared φ-shell to Principle-B .pronoun ([Cho81]'s elsewhere case for a pro-form).

Equations

• instBoundPronoun = { bindingClass := fun (p : Pronoun) => p.bindingClass.getD Features.BindingClass.pronoun }

@[implicit_reducible]

instance instBoundPersonalPronoun : Bound PersonalPronoun

Equations

• instBoundPersonalPronoun = { bindingClass := fun (p : PersonalPronoun) => p.bindingClass.getD Features.BindingClass.pronoun }

theorem bindingClassOf_toWord (p : Pronoun) (h : p.bindingClass ≠ some Features.BindingClass.rExpression) (hr : p.pronType = some UD.PronType.Rcp → p.bindingClass = some Features.BindingClass.reciprocal) : Binding.bindingClassOf p.toWord = Bound.source p

The canonical morphology source agrees with the mixin: a pro-form's projected word classifies (Binding.bindingClassOf, reading Reflex/PronType/category) exactly as the carrier's Bound class — Pronoun.toWord threads the binding morphology faithfully, so the surface engine and the capability never diverge. Two coherence premises, both vacuous for every actual entry: the pronoun is not lexically declared an R-expression (its surface category .PRON would win), and it does not store PronType=Rcp (reciprocal is derived by toWord from bindingClass = .reciprocal, never stored).

The number axis: HasNumber instances and faithfulness

@[implicit_reducible]

instance instHasNumberPronoun : HasNumber Pronoun

A pronoun bears its analytical number directly — the carrier field is root-Number-typed.

Equations

• instHasNumberPronoun = { numberOf := fun (p : Pronoun) => p.number }

@[implicit_reducible]

instance instHasNumberPersonalPronoun : HasNumber PersonalPronoun

Equations

• instHasNumberPersonalPronoun = { numberOf := fun (p : PersonalPronoun) => HasNumber.numberOf p.toPronoun }

theorem numberOf_toWord (p : Pronoun) : HasNumber.numberOf p.toWord = p.number.bind fun (n : Number) => n.toUD.bind Number.fromUD

Projecting a pronoun to a Word realizes its number through UD: the round-trip is identity exactly on UD-expressible values — the minimal/augmented values are lost to realization (Number.toUD is partial), the number analogue of personOf_toWord's coarsening.

The person axis: HasPerson instances and faithfulness

@[implicit_reducible]

instance instHasPersonPronoun : HasPerson Pronoun

A pronoun bears its analytical person directly — the carrier field is root-Person-typed, clusivity included (Tagalog kami = firstExclusive).

Equations

• instHasPersonPronoun = { personOf := fun (p : Pronoun) => p.person }

@[implicit_reducible]

instance instHasPersonPersonalPronoun : HasPerson PersonalPronoun

Equations

• instHasPersonPersonalPronoun = { personOf := fun (p : PersonalPronoun) => personOf p.toPronoun }

theorem personOf_toWord (p : Pronoun) : personOf p.toWord = Option.map Person.coarsen (personOf p)

Projecting a pronoun to a Word coarsens its person: Word carries UD realization, which has no clusivity — the mixin makes the loss explicit rather than silent.

The case axis: HasCase instances and faithfulness

@[implicit_reducible]

instance instHasCasePronoun : HasCase Pronoun

A pronoun bears its analytical case directly — the carrier field is root-Case-typed.

Equations

• instHasCasePronoun = { caseOf := fun (p : Pronoun) => p.case_ }

@[implicit_reducible]

instance instHasCasePersonalPronoun : HasCase PersonalPronoun

Equations

• instHasCasePersonalPronoun = { caseOf := fun (p : PersonalPronoun) => caseOf p.toPronoun }

theorem caseOf_toWord (p : Pronoun) : caseOf p.toWord = caseOf p

Projecting a pronoun to a Word realizes its case through UD losslessly: Case.toUD is currently a bijection, so — unlike person (clusivity lost) and number (minimal/augmented lost) — the round-trip is the identity. This is the theorem that degrades when an analytical refinement splits a UD cell (Case.fromUD_toUD).

Orthogonal data-mixin: Deictic

class Deictic (α : Type u_1) [Proform α] : Type u_1

A deictic carrier exposes register and — when it diverges from agreement person — referential person, the features specific to personal/referential pronouns ([AZ25a]).

• register : α → Features.Register.Level

  Register level (T/V, honorific tiers).

• referentialPerson : α → Option Person

  Referential person when it diverges from formal/agreement person; none otherwise.

@[implicit_reducible]

instance instDeicticPersonalPronoun : Deictic PersonalPronoun

Equations

• instDeicticPersonalPronoun = { register := PersonalPronoun.register, referentialPerson := PersonalPronoun.referentialPerson }