inductive AlokBhalla2026.AMType : Type

Morphosyntactic type of allocutive marker ([PPZ19] §2).

• agreeMorpheme : AMType
• particle : AMType
• cliticPronoun : AMType

def AlokBhalla2026.instReprAMType.repr : AMType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlokBhalla2026.instReprAMType : Repr AMType

Equations

• AlokBhalla2026.instReprAMType = { reprPrec := AlokBhalla2026.instReprAMType.repr }

@[implicit_reducible]

instance AlokBhalla2026.instDecidableEqAMType : DecidableEq AMType

Equations

• AlokBhalla2026.instDecidableEqAMType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive AlokBhalla2026.Embeddability : Type

Distribution across clause types ([PPZ19] §3.1).

• rootOnly : Embeddability
• limitedEmbed : Embeddability
• freelyEmbed : Embeddability

def AlokBhalla2026.instReprEmbeddability.repr : Embeddability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlokBhalla2026.instReprEmbeddability : Repr Embeddability

Equations

• AlokBhalla2026.instReprEmbeddability = { reprPrec := AlokBhalla2026.instReprEmbeddability.repr }

@[implicit_reducible]

instance AlokBhalla2026.instDecidableEqEmbeddability : DecidableEq Embeddability

Equations

• AlokBhalla2026.instDecidableEqEmbeddability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive AlokBhalla2026.HonDomain : Type

Where honorification surfaces.

• verbal : HonDomain
• nominal : HonDomain
• both : HonDomain

@[implicit_reducible]

instance AlokBhalla2026.instReprHonDomain : Repr HonDomain

Equations

• AlokBhalla2026.instReprHonDomain = { reprPrec := AlokBhalla2026.instReprHonDomain.repr }

def AlokBhalla2026.instReprHonDomain.repr : HonDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlokBhalla2026.instDecidableEqHonDomain : DecidableEq HonDomain

Equations

• AlokBhalla2026.instDecidableEqHonDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure AlokBhalla2026.AllocDatum : Type

A single allocutive datum: one language's profile.

• language : String
• amType : AMType
• embeddability : Embeddability
• hasTV : Bool

  Whether the language has a T/V pronoun distinction

• has3PHon : Bool

  Whether 3rd person honorifics exist

• domain : HonDomain

  Where honorification is realized

@[implicit_reducible]

instance AlokBhalla2026.instReprAllocDatum : Repr AllocDatum

Equations

• AlokBhalla2026.instReprAllocDatum = { reprPrec := AlokBhalla2026.instReprAllocDatum.repr }

def AlokBhalla2026.instReprAllocDatum.repr : AllocDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlokBhalla2026.instDecidableEqAllocDatum : DecidableEq AllocDatum

Equations

• AlokBhalla2026.instDecidableEqAllocDatum = AlokBhalla2026.instDecidableEqAllocDatum.decEq

def AlokBhalla2026.instDecidableEqAllocDatum.decEq (x✝ x✝¹ : AllocDatum) : Decidable (x✝ = x✝¹)

Equations

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

def AlokBhalla2026.basque : AllocDatum

Equations

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

def AlokBhalla2026.magahi : AllocDatum

Equations

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

def AlokBhalla2026.korean : AllocDatum

Equations

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

def AlokBhalla2026.japanese : AllocDatum

Equations

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

def AlokBhalla2026.tamil : AllocDatum

Equations

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

def AlokBhalla2026.galician : AllocDatum

Equations

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

def AlokBhalla2026.hindi : AllocDatum

Equations

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

def AlokBhalla2026.maithili : AllocDatum

Equations

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

def AlokBhalla2026.punjabi : AllocDatum

Equations

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

def AlokBhalla2026.allAllocData : List AllocDatum

Equations

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

theorem AlokBhalla2026.rootOnly_languages_exist : ∃ d ∈ allAllocData, d.embeddability = Embeddability.rootOnly

At least one language restricts allocutive marking to root clauses.

theorem AlokBhalla2026.freelyEmbed_languages_exist : ∃ d ∈ allAllocData, d.embeddability = Embeddability.freelyEmbed

At least one language freely embeds allocutive marking.

theorem AlokBhalla2026.all_have_verbal : (allAllocData.all fun (d : AllocDatum) => d.domain == HonDomain.verbal || d.domain == HonDomain.both) = true

All allocutive languages in the survey mark the verbal domain (verbal or both).

theorem AlokBhalla2026.all_have_tv : (allAllocData.all fun (d : AllocDatum) => d.hasTV) = true

All surveyed allocutive languages have a T/V pronoun distinction.

structure AlokBhalla2026.AllocAgree : Type

An allocutive Agree configuration: a probe (Fin or SA head) enters Agree with a null addressee DP bearing valued [iHON] and [person:2].

• probe : Minimalist.SyntacticObject

  The probe (Fin or SA head)

• probeFeatures : Minimalist.FeatureBundle

  Feature bundle on the probe (contains unvalued [uHON])

• addressee : Minimalist.SyntacticObject

  The null addressee DP

• addresseeFeatures : Minimalist.FeatureBundle

  Feature bundle on the addressee (valued [iHON], [person:2])

• probeCat : Minimalist.Cat

  Category of the probe: Fin or SA

def AlokBhalla2026.allocProbeFeatures (level : Minimalist.HonLevel) : Minimalist.FeatureBundle

Probe features for allocutive agreement: unvalued [uHON].

Equations

• AlokBhalla2026.allocProbeFeatures level = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.hon level)]

def AlokBhalla2026.addresseeDPFeatures (level : Minimalist.HonLevel) : Minimalist.FeatureBundle

Addressee DP features: valued [iHON] and [person:2]. The addressee is always 2nd person.

Equations

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

def AlokBhalla2026.predictEmbeddability : Minimalist.Cat → Embeddability

Predict embeddability from the category of the allocutive probe. SA → root-only (SAP does not embed), Fin → freely embeddable.

Equations

• AlokBhalla2026.predictEmbeddability Minimalist.Cat.SA = AlokBhalla2026.Embeddability.rootOnly
• AlokBhalla2026.predictEmbeddability Minimalist.Cat.Fin = AlokBhalla2026.Embeddability.freelyEmbed
• AlokBhalla2026.predictEmbeddability x✝ = AlokBhalla2026.Embeddability.limitedEmbed

theorem AlokBhalla2026.sa_probe_root_only : predictEmbeddability Minimalist.Cat.SA = Embeddability.rootOnly

theorem AlokBhalla2026.fin_probe_embeddable : predictEmbeddability Minimalist.Cat.Fin = Embeddability.freelyEmbed

def AlokBhalla2026.probeLocus : String → Minimalist.Cat

Probe-locus assignment for each language in the survey.

Equations

• AlokBhalla2026.probeLocus "Souletian Basque" = Minimalist.Cat.SA
• AlokBhalla2026.probeLocus "Korean" = Minimalist.Cat.SA
• AlokBhalla2026.probeLocus "Japanese" = Minimalist.Cat.SA
• AlokBhalla2026.probeLocus "Magahi" = Minimalist.Cat.Fin
• AlokBhalla2026.probeLocus "Galician" = Minimalist.Cat.Fin
• AlokBhalla2026.probeLocus "Hindi" = Minimalist.Cat.Fin
• AlokBhalla2026.probeLocus "Maithili" = Minimalist.Cat.Fin
• AlokBhalla2026.probeLocus "Tamil" = Minimalist.Cat.Fin
• AlokBhalla2026.probeLocus "Punjabi" = Minimalist.Cat.Fin
• AlokBhalla2026.probeLocus x✝ = Minimalist.Cat.C

def AlokBhalla2026.correctlyPredicts (d : AllocDatum) : Bool

Check that the predicted embeddability matches the observed data (modulo limited-embed, which Fin subsumes).

Equations

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

theorem AlokBhalla2026.all_correctly_predicted (d : AllocDatum) : d ∈ allAllocData → correctlyPredicts d = true

All languages in the survey are correctly predicted by probe locus.

structure AlokBhalla2026.HonRelation (E : Type u_1) : Type u_1

The [iHON] relation: encodes social hierarchy between speaker and referent. ⟦iHON⟧ = λx. S_i ≺ x, where ≺ is social ordering.

• speaker : E

  The speaker

• referent : E

  The referent (target of honorification)

• level : Minimalist.HonLevel

  The honorific level determined by the relation

structure AlokBhalla2026.HonP : Type

HonP: a functional projection in the nominal spine that hosts [iHON]. Wraps a DP's SO with an honorific feature.

• dp : Minimalist.SyntacticObject

  The underlying DP

• honFeature : Minimalist.GramFeature

  The honorific feature on HonP

• isHon : ∃ (l : Minimalist.HonLevel), self.honFeature = Minimalist.GramFeature.valued (Minimalist.FeatureVal.hon l)

  The feature must be a valued [iHON]

def AlokBhalla2026.HonP.level (hp : HonP) : Minimalist.HonLevel

Extract the honorific level from a HonP.

Equations

• hp.level = match hp.honFeature with | Minimalist.GramFeature.valued (Minimalist.FeatureVal.hon l) => l | x => Minimalist.HonLevel.nh

theorem AlokBhalla2026.aa_is_agree (rel : Minimalist.AgreeRelation) (root : Minimalist.SyntacticObject) (hValid : Minimalist.validAgree rel root) : Minimalist.validAgree rel root

AA validity reduces to validAgree: allocutive agreement is not special machinery — it IS phi-agreement between a functional head and a null addressee DP.

theorem AlokBhalla2026.sa_based_aa_root_only : predictEmbeddability Minimalist.Cat.SA = Embeddability.rootOnly

SA-based allocutive agreement is root-only. Follows directly from SAP being the highest phase.

theorem AlokBhalla2026.fin_based_aa_embeddable : predictEmbeddability Minimalist.Cat.Fin = Embeddability.freelyEmbed

Fin-based allocutive agreement is freely embeddable. FinP is below CP and embeds normally.

theorem AlokBhalla2026.basque_prediction : predictEmbeddability (probeLocus "Souletian Basque") = Embeddability.rootOnly

Basque prediction: probe = SA → root-only.

theorem AlokBhalla2026.magahi_prediction : predictEmbeddability (probeLocus "Magahi") = Embeddability.freelyEmbed

Magahi prediction: probe = Fin → freely embeddable.

theorem AlokBhalla2026.korean_prediction : predictEmbeddability (probeLocus "Korean") = Embeddability.rootOnly

Korean prediction: probe = SA (particle-based) → root-only.

theorem AlokBhalla2026.hon_features_match (level : Minimalist.HonLevel) : Minimalist.featuresMatch (Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.hon level)) (Minimalist.GramFeature.valued (Minimalist.FeatureVal.hon level)) = true

[iHON] features match under Agree: probe [uHON] can be valued by goal [iHON], paralleling standard phi-agreement.

theorem AlokBhalla2026.hon_agree_values (level : Minimalist.HonLevel) : Minimalist.applyAgree (allocProbeFeatures level) (addresseeDPFeatures level) (Minimalist.FeatureVal.hon level) = some (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.hon level)])

Honorific valuation via Agree: applying Agree to an allocutive probe with [uHON] against an addressee with [iHON] values the probe.

theorem AlokBhalla2026.sa_alloc_parallels_sa_questions : predictEmbeddability Minimalist.Cat.SA = Embeddability.rootOnly ∧ (allAllocData.all fun (d : AllocDatum) => if (probeLocus d.language == Minimalist.Cat.SA) = true then d.embeddability == Embeddability.rootOnly else true) = true

Bridge to Studies/BhattDayal2020: SAP unembeddability parallels sap_particles_not_in_quasi_sub. Both follow from SAP being the speech-act layer that does not embed.

Connection: SA-based allocutive markers (particles) pattern with SAP-layer question particles — neither appears in quasi-subordination. This is a structural parallel, not an identity theorem.

theorem AlokBhalla2026.hon_levels_ordered (l : Minimalist.HonLevel) : l = Minimalist.HonLevel.nh ∨ l = Minimalist.HonLevel.h ∨ l = Minimalist.HonLevel.hh

Bridge to [YTGF20] politeness: social utility (φ weighting informational vs social goals) is the pragmatic analogue of syntactic [iHON]. Both encode social relations between discourse participants.

[iHON] is syntactic: speaker ≺ referent in the grammar. Social utility is pragmatic: speaker optimizes face preservation. The parallel: honorific level increases ↔ social weight φ increases.

def AlokBhalla2026.levelToHonLevel : Features.Register.Level → Minimalist.HonLevel

Convert register level to theory HonLevel. informal → non-honorific, neutral → honorific, formal → high-honorific.

Equations

• AlokBhalla2026.levelToHonLevel Features.Register.Level.informal = Minimalist.HonLevel.nh
• AlokBhalla2026.levelToHonLevel Features.Register.Level.neutral = Minimalist.HonLevel.h
• AlokBhalla2026.levelToHonLevel Features.Register.Level.formal = Minimalist.HonLevel.hh

theorem AlokBhalla2026.basque_fragment_has_2p : (Basque.Pronouns.secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

Basque fragment has 2nd-person pronouns.

theorem AlokBhalla2026.magahi_fragment_three_levels : List.map (fun (x : PersonalPronoun) => x.register) Magahi.Pronouns.secondPersonPronouns = [Features.Register.Level.informal, Features.Register.Level.neutral, Features.Register.Level.formal]

Magahi fragment has three honorific levels.

theorem AlokBhalla2026.korean_fragment_has_2p : (Korean.Pronouns.secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

Korean fragment has 2nd-person pronouns.

theorem AlokBhalla2026.japanese_fragment_has_2p : (Japanese.Pronouns.secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

Japanese fragment has 2nd-person pronouns.

theorem AlokBhalla2026.tamil_fragment_has_2p : (Tamil.Pronouns.secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

Tamil fragment has 2nd-person pronouns.

theorem AlokBhalla2026.galician_fragment_has_2p : (Galician.Pronouns.secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

Galician fragment has 2nd-person pronouns.

theorem AlokBhalla2026.hindi_fragment_three_levels : List.map (fun (x : PersonalPronoun) => x.register) Hindi.Pronouns.secondPersonPronouns = [Features.Register.Level.informal, Features.Register.Level.neutral, Features.Register.Level.formal]

Hindi fragment has three honorific levels.

theorem AlokBhalla2026.maithili_fragment_three_levels : List.map (fun (x : PersonalPronoun) => x.register) Maithili.Pronouns.secondPersonPronouns = [Features.Register.Level.informal, Features.Register.Level.neutral, Features.Register.Level.formal]

Maithili fragment has three honorific levels.

theorem AlokBhalla2026.punjabi_fragment_has_2p : (Punjabi.Pronouns.secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

Punjabi fragment has 2nd-person pronouns.

theorem AlokBhalla2026.informal_nh : levelToHonLevel Features.Register.Level.informal = Minimalist.HonLevel.nh

Register bridge: informal maps to non-honorific.

theorem AlokBhalla2026.neutral_h : levelToHonLevel Features.Register.Level.neutral = Minimalist.HonLevel.h

Register bridge: neutral maps to honorific.

theorem AlokBhalla2026.formal_hh : levelToHonLevel Features.Register.Level.formal = Minimalist.HonLevel.hh

Register bridge: formal maps to high-honorific.