structure Minimalism.Phenomena.Allocutivity.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 : SyntacticObject

  The probe (Fin or SA head)

• probeFeatures : FeatureBundle

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

• addressee : SyntacticObject

  The null addressee DP

• addresseeFeatures : FeatureBundle

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

• probeCat : Cat

  Category of the probe: Fin or SA

def Minimalism.Phenomena.Allocutivity.allocProbeFeatures (level : HonLevel) : FeatureBundle

Probe features for allocutive agreement: unvalued [uHON].

Equations

• Minimalism.Phenomena.Allocutivity.allocProbeFeatures level = [Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.hon level)]

def Minimalism.Phenomena.Allocutivity.addresseeDPFeatures (level : HonLevel) : 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 Minimalism.Phenomena.Allocutivity.predictEmbeddability : Cat → Phenomena.Politeness.Honorifics.Embeddability

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

Equations

• Minimalism.Phenomena.Allocutivity.predictEmbeddability Minimalism.Cat.SA = Phenomena.Politeness.Honorifics.Embeddability.rootOnly
• Minimalism.Phenomena.Allocutivity.predictEmbeddability Minimalism.Cat.Fin = Phenomena.Politeness.Honorifics.Embeddability.freelyEmbed
• Minimalism.Phenomena.Allocutivity.predictEmbeddability x✝ = Phenomena.Politeness.Honorifics.Embeddability.limitedEmbed

theorem Minimalism.Phenomena.Allocutivity.sa_probe_root_only : predictEmbeddability Cat.SA = Phenomena.Politeness.Honorifics.Embeddability.rootOnly

theorem Minimalism.Phenomena.Allocutivity.fin_probe_embeddable : predictEmbeddability Cat.Fin = Phenomena.Politeness.Honorifics.Embeddability.freelyEmbed

def Minimalism.Phenomena.Allocutivity.probeLocus : String → Cat

Probe-locus assignment for each language in the survey.

Equations

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

def Minimalism.Phenomena.Allocutivity.correctlyPredicts (d : Phenomena.Politeness.Honorifics.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 Minimalism.Phenomena.Allocutivity.all_correctly_predicted (d : Phenomena.Politeness.Honorifics.AllocDatum) : d ∈ Phenomena.Politeness.Honorifics.allAllocData → correctlyPredicts d = true

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

structure Minimalism.Phenomena.Allocutivity.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 : HonLevel

  The honorific level determined by the relation

structure Minimalism.Phenomena.Allocutivity.HonP : Type

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

• dp : SyntacticObject

  The underlying DP

• honFeature : GramFeature

  The honorific feature on HonP

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

  The feature must be a valued [iHON]

def Minimalism.Phenomena.Allocutivity.HonP.level (hp : HonP) : HonLevel

Extract the honorific level from a HonP.

Equations

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

theorem Minimalism.Phenomena.Allocutivity.aa_is_agree (rel : AgreeRelation) (root : SyntacticObject) (hValid : validAgree rel root) : 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 Minimalism.Phenomena.Allocutivity.sa_based_aa_root_only : predictEmbeddability Cat.SA = Phenomena.Politeness.Honorifics.Embeddability.rootOnly

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

theorem Minimalism.Phenomena.Allocutivity.fin_based_aa_embeddable : predictEmbeddability Cat.Fin = Phenomena.Politeness.Honorifics.Embeddability.freelyEmbed

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

theorem Minimalism.Phenomena.Allocutivity.basque_prediction : predictEmbeddability (probeLocus "Souletian Basque") = Phenomena.Politeness.Honorifics.Embeddability.rootOnly

Basque prediction: probe = SA → root-only.

theorem Minimalism.Phenomena.Allocutivity.magahi_prediction : predictEmbeddability (probeLocus "Magahi") = Phenomena.Politeness.Honorifics.Embeddability.freelyEmbed

Magahi prediction: probe = Fin → freely embeddable.

theorem Minimalism.Phenomena.Allocutivity.korean_prediction : predictEmbeddability (probeLocus "Korean") = Phenomena.Politeness.Honorifics.Embeddability.rootOnly

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

theorem Minimalism.Phenomena.Allocutivity.hon_features_match (level : HonLevel) : featuresMatch (GramFeature.unvalued (FeatureVal.hon level)) (GramFeature.valued (FeatureVal.hon level)) = true

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

theorem Minimalism.Phenomena.Allocutivity.hon_agree_values (level : HonLevel) : applyAgree (allocProbeFeatures level) (addresseeDPFeatures level) (FeatureVal.hon level) = some [GramFeature.valued (FeatureVal.hon level)]

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

theorem Minimalism.Phenomena.Allocutivity.sa_alloc_parallels_sa_questions : predictEmbeddability Cat.SA = Phenomena.Politeness.Honorifics.Embeddability.rootOnly ∧ (Phenomena.Politeness.Honorifics.allAllocData.all fun (d : Phenomena.Politeness.Honorifics.AllocDatum) => if (probeLocus d.language == Cat.SA) = true then d.embeddability == Phenomena.Politeness.Honorifics.Embeddability.rootOnly else true) = true

Bridge to Phenomena/Questions/Typology: 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 Minimalism.Phenomena.Allocutivity.hon_levels_ordered (l : HonLevel) : l = HonLevel.nh ∨ l = HonLevel.h ∨ l = HonLevel.hh

Bridge to @cite{yoon-etal-2020} 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 Minimalism.Phenomena.Allocutivity.levelToHonLevel : Core.Register.Level → HonLevel

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

Equations

• Minimalism.Phenomena.Allocutivity.levelToHonLevel Core.Register.Level.informal = Minimalism.HonLevel.nh
• Minimalism.Phenomena.Allocutivity.levelToHonLevel Core.Register.Level.neutral = Minimalism.HonLevel.h
• Minimalism.Phenomena.Allocutivity.levelToHonLevel Core.Register.Level.formal = Minimalism.HonLevel.hh

theorem Minimalism.Phenomena.Allocutivity.basque_fragment_has_2p : (Fragments.Basque.Pronouns.secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

Basque fragment has 2nd-person pronouns.

theorem Minimalism.Phenomena.Allocutivity.magahi_fragment_three_levels : List.map (fun (x : Core.Pronouns.PronounEntry) => x.register) Fragments.Magahi.Pronouns.secondPersonPronouns = [Core.Register.Level.informal, Core.Register.Level.neutral, Core.Register.Level.formal]

Magahi fragment has three honorific levels.

theorem Minimalism.Phenomena.Allocutivity.korean_fragment_has_2p : (Fragments.Korean.Pronouns.secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

Korean fragment has 2nd-person pronouns.

theorem Minimalism.Phenomena.Allocutivity.japanese_fragment_has_2p : (Fragments.Japanese.Pronouns.secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

Japanese fragment has 2nd-person pronouns.

theorem Minimalism.Phenomena.Allocutivity.tamil_fragment_has_2p : (Fragments.Tamil.Pronouns.secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

Tamil fragment has 2nd-person pronouns.

theorem Minimalism.Phenomena.Allocutivity.galician_fragment_has_2p : (Fragments.Galician.Pronouns.secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

Galician fragment has 2nd-person pronouns.

theorem Minimalism.Phenomena.Allocutivity.hindi_fragment_three_levels : List.map (fun (x : Core.Pronouns.PronounEntry) => x.register) Fragments.Hindi.Pronouns.secondPersonPronouns = [Core.Register.Level.informal, Core.Register.Level.neutral, Core.Register.Level.formal]

Hindi fragment has three honorific levels.

theorem Minimalism.Phenomena.Allocutivity.maithili_fragment_three_levels : List.map (fun (x : Core.Pronouns.PronounEntry) => x.register) Fragments.Maithili.Pronouns.secondPersonPronouns = [Core.Register.Level.informal, Core.Register.Level.neutral, Core.Register.Level.formal]

Maithili fragment has three honorific levels.

theorem Minimalism.Phenomena.Allocutivity.punjabi_fragment_has_2p : (Fragments.Punjabi.Pronouns.secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

Punjabi fragment has 2nd-person pronouns.

theorem Minimalism.Phenomena.Allocutivity.informal_nh : levelToHonLevel Core.Register.Level.informal = HonLevel.nh

Register bridge: informal maps to non-honorific.

theorem Minimalism.Phenomena.Allocutivity.neutral_h : levelToHonLevel Core.Register.Level.neutral = HonLevel.h

Register bridge: neutral maps to honorific.

theorem Minimalism.Phenomena.Allocutivity.formal_hh : levelToHonLevel Core.Register.Level.formal = HonLevel.hh

Register bridge: formal maps to high-honorific.