DM Vocabulary Insertion under Containment Locality

@cite{bobaljik-2012} @cite{bobaljik-2000} @cite{halle-marantz-1993} @cite{smith-moskal-xu-kang-bobaljik-2019}

The DM-flavored derivation of the *ABA generalization for inflectional morphology under root-out Vocabulary Insertion (@cite{bobaljik-2000}): root VI rules can only be conditioned on features inside their local domain, which means the same VI rule set competes at multiple cells of a containment hierarchy and the Elsewhere mechanism picks identical winners — giving plateau behavior, hence *ABA exclusion.

This file is the DM-side derivation of substrate facts in Core/Morphology/Containment.lean and Core/Morphology/DegreeContainment.lean. The Nanosyntax-side derivation (Superset Principle on phrasal spellout) would live in Theories/Morphology/Nanosyntax/.

File layout — two layers

PART I (n-parametric, §§1–6): the general containment-VI machinery, parameterized by hierarchy depth n. The headline lemma is applicableRules_sublist_of_le — under root-out locality, the set of applicable rules is monotone in position. From monotonicity + a locality cap M (no rule has contextLevel > M), the function viWinner is constant on positions p ≥ M (the plateau theorem viWinningContextLevel_const_above_cap). Specialized to n = 3, M = 1 this is the comparative-superlative result vi_cmpr_eq_sprl.

PART II (degree specialization, §§7–9, sub-namespace Degree): the n=3 degree case derived from PART I via subtype refinement. Degree.LocalVIRule := { r : ContainmentVIRule 3 // r.contextLevel ≤ cmprLevel } bundles the locality cap into the rule type (mathlib OrderHom idiom). Degree.vi_cmpr_eq_sprl is a one-line corollary of PART I's viExponent_const_above_cap. Consumers (Bobaljik2012, SmithMoskalEtAl2019) keep their DegreePattern-typed signatures unchanged — Degree.viPattern still returns DegreePattern.

The deep mathematical content

The headline lemma applicableRules_sublist_of_le is structural and pre-morphological: as a position climbs from POS to SPRL (degree), ABS to OBL (case), or SG to DL (number), strictly more rules become applicable — those whose conditioning context is contained in the current position. The remaining lemmas in PART I are pure plumbing on this monotone structure:

• applicableRules_eq_squeeze: when the applicable sets at two endpoints p ≤ r agree, every position q squeezed between them has the same applicable set. Structural analog of Monotone.eq_of_le_of_le.
• viWinner_eq_of_applicableRules_eq: when applicable sets agree, the Elsewhere mechanism picks the same winner.
• applicableRules_eq_above_cap: under the cap, all positions ≥ M share the same applicable set.
• viWinningContextLevel_const_above_cap: combine to get plateau.

For the bridge to Morphology.Containment.ViolatesABA, see PART II's vi_cmpr_eq_sprl (n=3 case directly) or apply viExponent_const_above_cap at adjacent positions in the n>3 case.

Future work

The Theories/Morphology/Nanosyntax/ parallel — phrasal spellout + Superset Principle deriving the same *ABA exclusion — is a separate file the substrate anticipates but does not yet exist.

structure Theories.Morphology.DM.ContainmentVI.ContainmentVIRule (n : ℕ) : Type

A Vocabulary Insertion rule for an n-position containment hierarchy.

• exponent is the phonological form inserted at the terminal.
• contextLevel is the deepest position whose features the rule's context refers to. Under root-out insertion (@cite{bobaljik-2000}), the rule applies at any position p such that contextLevel ≤ p (positions strictly contain the contextLevel cell's features).
• specificity is the Elsewhere ranking (higher = more specific). When two rules both apply, the higher-specificity one wins.

The locality cap from @cite{bobaljik-2012} is not baked into the structure; it is a separate hypothesis on rule lists in §6.

• exponent : ℕ

  Phonological exponent inserted at the terminal.

• contextLevel : Fin n

  Deepest position whose features condition this rule.

• specificity : ℕ

  Specificity for Elsewhere ordering.

def Theories.Morphology.DM.ContainmentVI.instDecidableEqContainmentVIRule.decEq {n✝ : ℕ} (x✝ x✝¹ : ContainmentVIRule n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Theories.Morphology.DM.ContainmentVI.instDecidableEqContainmentVIRule {n✝ : ℕ} : DecidableEq (ContainmentVIRule n✝)

Equations

• Theories.Morphology.DM.ContainmentVI.instDecidableEqContainmentVIRule = Theories.Morphology.DM.ContainmentVI.instDecidableEqContainmentVIRule.decEq

def Theories.Morphology.DM.ContainmentVI.instReprContainmentVIRule.repr {n✝ : ℕ} : ContainmentVIRule n✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Theories.Morphology.DM.ContainmentVI.instReprContainmentVIRule {n✝ : ℕ} : Repr (ContainmentVIRule n✝)

Equations

• Theories.Morphology.DM.ContainmentVI.instReprContainmentVIRule = { reprPrec := Theories.Morphology.DM.ContainmentVI.instReprContainmentVIRule.repr }

def Theories.Morphology.DM.ContainmentVI.ContainmentVIRule.AppliesAt {n : ℕ} (r : ContainmentVIRule n) (p : Fin n) : Prop

A rule applies at position p iff its contextLevel is ≤ p (root-out: outer positions can be conditioned on inner features).

Equations

• r.AppliesAt p = (r.contextLevel ≤ p)

@[implicit_reducible]

instance Theories.Morphology.DM.ContainmentVI.instDecidableAppliesAt {n : ℕ} (r : ContainmentVIRule n) (p : Fin n) : Decidable (r.AppliesAt p)

Equations

• Theories.Morphology.DM.ContainmentVI.instDecidableAppliesAt r p = Theories.Morphology.DM.ContainmentVI.instDecidableAppliesAt._aux_1 r p

theorem Theories.Morphology.DM.ContainmentVI.ContainmentVIRule.AppliesAt.mono {n : ℕ} {r : ContainmentVIRule n} {p q : Fin n} (h : p ≤ q) : r.AppliesAt p → r.AppliesAt q

Applicability is monotone in position: if a rule applies at p and p ≤ q, it applies at q.

def Theories.Morphology.DM.ContainmentVI.applicableRules {n : ℕ} (rules : List (ContainmentVIRule n)) (p : Fin n) : List (ContainmentVIRule n)

The list of rules applicable at position p, preserving the order of the input list (so Elsewhere ties break by source order).

Equations

• Theories.Morphology.DM.ContainmentVI.applicableRules rules p = List.filter (fun (r : Theories.Morphology.DM.ContainmentVI.ContainmentVIRule n) => decide (r.AppliesAt p)) rules

@[simp]

theorem Theories.Morphology.DM.ContainmentVI.mem_applicableRules {n : ℕ} {rules : List (ContainmentVIRule n)} {p : Fin n} {r : ContainmentVIRule n} : r ∈ applicableRules rules p ↔ r ∈ rules ∧ r.AppliesAt p

theorem Theories.Morphology.DM.ContainmentVI.applicableRules_sublist_of_le {n : ℕ} (rules : List (ContainmentVIRule n)) {p q : Fin n} (h : p ≤ q) : (applicableRules rules p).Sublist (applicableRules rules q)

Headline structural lemma. As the position climbs the containment hierarchy, the set of applicable rules grows monotonically. This is the deep mathematical content from which *ABA exclusion follows in two further short steps (§4, §6).

Stated as List.Sublist: every rule applicable at the lower position is applicable at the higher position, in the same order.

theorem Theories.Morphology.DM.ContainmentVI.applicableRules_subset_of_le {n : ℕ} (rules : List (ContainmentVIRule n)) {p q : Fin n} (h : p ≤ q) : {r : ContainmentVIRule n | r ∈ applicableRules rules p} ⊆ {r : ContainmentVIRule n | r ∈ applicableRules rules q}

The rule-set form (Set inclusion). The Set-level statement is the canonical mathlib idiom for Monotone of a function into a powerset lattice; the List.Sublist form above is the constructive analog that respects Elsewhere's source-order tie-breaking.

theorem Theories.Morphology.DM.ContainmentVI.applicableRules_eq_squeeze {n : ℕ} (rules : List (ContainmentVIRule n)) {p q r : Fin n} (h_pq : p ≤ q) (h_qr : q ≤ r) (h_pr : applicableRules rules p = applicableRules rules r) : applicableRules rules q = applicableRules rules p

Squeeze lemma. When applicableRules at two endpoints p ≤ r agree, every position q between them has the same applicable set.

Pure-list reasoning: under monotonicity (§3), the middle filter is sandwiched between the equal endpoint filters, forcing equality. This is the structural analog of Monotone.eq_of_le_of_le.

def Theories.Morphology.DM.ContainmentVI.viWinner {n : ℕ} (rules : List (ContainmentVIRule n)) (p : Fin n) : Option (ContainmentVIRule n)

The winning rule at position p: highest-specificity applicable rule. mergeSort is stable, so ties break by input-list order (the standard interpretation of Elsewhere when specificities tie).

Equations

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

def Theories.Morphology.DM.ContainmentVI.viWinningContextLevel {n : ℕ} (rules : List (ContainmentVIRule n)) (p : Fin n) : WithBot (Fin n)

The contextLevel of the winning rule at position p, as WithBot (Fin n) (returns ⊥ if no rule applies).

Equations

• Theories.Morphology.DM.ContainmentVI.viWinningContextLevel rules p = match Theories.Morphology.DM.ContainmentVI.viWinner rules p with | some r => ↑r.contextLevel | none => ⊥

def Theories.Morphology.DM.ContainmentVI.viExponent {n : ℕ} (rules : List (ContainmentVIRule n)) (defaultForm : ℕ) (p : Fin n) : ℕ

The exponent of the winning rule at position p, falling back to defaultForm if no rule applies.

Equations

• Theories.Morphology.DM.ContainmentVI.viExponent rules defaultForm p = match Theories.Morphology.DM.ContainmentVI.viWinner rules p with | some r => r.exponent | none => defaultForm

def Theories.Morphology.DM.ContainmentVI.viCellPattern {n : ℕ} (rules : List (ContainmentVIRule n)) (defaultForm : ℕ) : List ℕ

The realized cell pattern: list of exponents at each of the n positions, in containment order.

Equations

• Theories.Morphology.DM.ContainmentVI.viCellPattern rules defaultForm = List.map (Theories.Morphology.DM.ContainmentVI.viExponent rules defaultForm) (List.finRange n)

theorem Theories.Morphology.DM.ContainmentVI.viWinner_eq_of_applicableRules_eq {n : ℕ} {rules : List (ContainmentVIRule n)} {p q : Fin n} (h : applicableRules rules p = applicableRules rules q) : viWinner rules p = viWinner rules q

Bridge lemma. The viWinner function depends only on applicableRules: when applicable sets agree, the same Elsewhere competition picks the same winner.

theorem Theories.Morphology.DM.ContainmentVI.viExponent_eq_of_applicableRules_eq {n : ℕ} {rules : List (ContainmentVIRule n)} {defaultForm : ℕ} {p q : Fin n} (h : applicableRules rules p = applicableRules rules q) : viExponent rules defaultForm p = viExponent rules defaultForm q

Corollary: when applicable sets agree, exponent agrees.

def Theories.Morphology.DM.ContainmentVI.CappedAt {n : ℕ} (rules : List (ContainmentVIRule n)) (M : Fin n) : Prop

A rule list is capped at level M when no rule has contextLevel strictly above M. This is @cite{bobaljik-2012}'s containment locality: root VI rules can be conditioned only on the immediately containing functional head, not on more distant ones.

Equations

• Theories.Morphology.DM.ContainmentVI.CappedAt rules M = ∀ r ∈ rules, r.contextLevel ≤ M

theorem Theories.Morphology.DM.ContainmentVI.applicableRules_eq_above_cap {n : ℕ} {rules : List (ContainmentVIRule n)} {M : Fin n} (hCap : CappedAt rules M) {p q : Fin n} (hp : M ≤ p) (hq : M ≤ q) : applicableRules rules p = applicableRules rules q

Under the cap, applicable sets at positions p, q ≥ M agree. Both filters select the same set: every rule in the list (since every rule has contextLevel ≤ M ≤ p, q).

theorem Theories.Morphology.DM.ContainmentVI.viExponent_const_above_cap {n : ℕ} {rules : List (ContainmentVIRule n)} {M : Fin n} (hCap : CappedAt rules M) (defaultForm : ℕ) {p q : Fin n} (hp : M ≤ p) (hq : M ≤ q) : viExponent rules defaultForm p = viExponent rules defaultForm q

Plateau theorem. Under the cap, viExponent is constant on positions p, q ≥ M. Specializing to n = 3, M = 1 recovers Degree.vi_cmpr_eq_sprl (PART II).

theorem Theories.Morphology.DM.ContainmentVI.viWinningContextLevel_const_above_cap {n : ℕ} {rules : List (ContainmentVIRule n)} {M : Fin n} (hCap : CappedAt rules M) {p q : Fin n} (hp : M ≤ p) (hq : M ≤ q) : viWinningContextLevel rules p = viWinningContextLevel rules q

Headline corollary (n-position generalization of Degree.vi_cmpr_eq_sprl). Under the cap at M, viWinningContextLevel is constant on positions p ≥ M.

def Theories.Morphology.DM.ContainmentVI.Degree.cmprLevel : Fin 3

The locality cap for degree morphology: CMPR is the deepest position whose features a root VI rule can be conditioned on.

Equations

• Theories.Morphology.DM.ContainmentVI.Degree.cmprLevel = ⟨1, Theories.Morphology.DM.ContainmentVI.Degree.cmprLevel._proof_1⟩

@[reducible, inline]

abbrev Theories.Morphology.DM.ContainmentVI.Degree.LocalVIRule : Type

A locality-constrained VI rule for root morphemes in degree contexts (@cite{bobaljik-2012}, @cite{bobaljik-2000}).

Subtype of ContainmentVIRule 3 with the locality cap ≤ cmprLevel bundled in via subtype refinement. This is the mathlib OrderHom idiom (bundle the constraint with the carrier) applied to a morphological rule with a structural locality property.

Root-out insertion (@cite{bobaljik-2000}) means root VI rules can only be conditioned on features in the root's local domain — the CMPR head that immediately contains the root. The SPRL head is outside CMPR and invisible to root VI; this is the cap.

Equations

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

def Theories.Morphology.DM.ContainmentVI.Degree.viPattern (rules : List LocalVIRule) (defaultForm : ℕ) : Core.Morphology.DegreeContainment.DegreePattern

The degree pattern generated by VI competition. Built directly from PART I's viExponent, applied at each grade's position via DegreeGrade.toFin (defined in Core/Morphology/DegreeContainment.lean).

Equations

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

theorem Theories.Morphology.DM.ContainmentVI.Degree.vi_cmpr_eq_sprl (rules : List LocalVIRule) (defaultForm : ℕ) : (viPattern rules defaultForm).cmpr = (viPattern rules defaultForm).sprl

Core result: under degree locality, VI selects the same root form at CMPR and SPRL. Direct corollary of PART I's plateau theorem viExponent_const_above_cap at the cap cmprLevel, instantiated at positions 1 (CMPR) and 2 (SPRL).

Formal content of @cite{bobaljik-2012}'s containment argument: root suppletion at SPRL ↔ root suppletion at CMPR.

theorem Theories.Morphology.DM.ContainmentVI.Degree.csg_part1_vi (rules : List LocalVIRule) (defaultForm : ℕ) (h : (viPattern rules defaultForm).CmprSuppletive) : (viPattern rules defaultForm).SprlSuppletive

CSG Part I from VI: root suppletive at CMPR ⇒ root suppletive at SPRL.

theorem Theories.Morphology.DM.ContainmentVI.Degree.csg_part2_vi (rules : List LocalVIRule) (defaultForm : ℕ) (h : (viPattern rules defaultForm).SprlSuppletive) : (viPattern rules defaultForm).CmprSuppletive

CSG Part II from VI: root suppletive at SPRL ⇒ root suppletive at CMPR.

theorem Theories.Morphology.DM.ContainmentVI.Degree.vi_cmpr_eq_sprl_corollary (rules : List LocalVIRule) (defaultForm : ℕ) : (viPattern rules defaultForm).cmpr = (viPattern rules defaultForm).sprl

VI-generated root suppletion patterns are AAA or ABB only. *ABA is excluded by contiguity; *AAB and ABC (for root suppletion) are excluded by VI locality (CMPR cell = SPRL cell).