Vocabularies over containment hierarchies: Elsewhere insertion

[Bob12] [HM93] [Kip73]

The realizational engine behind [Bob12]'s comparative-suppletion generalizations, stated over an arbitrary n-grade containment hierarchy. An ExponenceRule realizes the initial span [0, spans] of the hierarchy (the root, possibly fused with the first spans heads — the portmanteau exponence of [Bob12]'s ch. 5, via Fusion (196) or Radkevich's Vocabulary Insertion Principle (197)), optionally conditioned on the presence of a higher head. Selection at each grade is by the Elsewhere Condition ([Kip73]): the most specific applicable rule wins, where Pāṇinian specificity is derived as applicability-set inclusion (ExponenceRule.moreSpecific_iff_threshold_le) — over a linear hierarchy applicability sets are nested upward sets, so the Elsewhere ordering is total.

Each of [Bob12]'s generalizations is a theorem with its own hypothesis set, mirroring the book's cost accounting:

• CSG1 / *ABA (isContiguous_realize): Antihomophony alone — the book's ch. 2 derivation from containment + Elsewhere + the antihomophony assumption (44). The homophony loophole is real: a non-antihomophonous vocabulary generating surface ABA is exhibited in Studies/Bobaljik2012.lean.
• Completeness (isContiguous_iff_generable): generable = contiguous over terminal antihomophonous vocabularies.
• The plateau (realize_const_of_terminal_adjacent): terminal rules + adjacent contexts generate only {AAA, ABB} — the Bobaljik-minus-portmanteaux fragment, which over-excludes the attested ABC (Latin bon- mel- opt-); portmanteau rules repair it.
• CSG2 / *AAB (csg2): Antihomophony + Grounded (the book's markedness condition (202)). The book blocks the two AAB routes by two mechanisms — adjacency for root-rules conditioned across an intervening head (190a), condition (202) for context-sensitive portmanteaux (201); under the threshold encoding both reduce to downward closure of the threshold set, so one hypothesis suffices.
• ABC requires a portmanteau (exists_portmanteau_of_ne; [Bob12] §5.3.1, the degree-domain consequence generalized there as (199)): under adjacency, superlative-grade root allomorphy distinct from the comparative grade arises only via a portmanteau rule.

Main declarations

• ExponenceRule n F — rule of exponence: exponent, exponed span [0, spans], optional conditioning head
• Terminal, Adjacent, Antihomophonous, Grounded — the axiom Props on vocabularies, à la carte
• winner, realize — Elsewhere selection and the realized pattern
• isContiguous_realize, isContiguous_iff_generable, realize_const_of_terminal_adjacent, csg2, exists_portmanteau_of_ne

The dual Superset engine lives in Morphology/Containment/Superset.lean; synthetic/analytic structure (Merger) in Morphology/Containment/Merger.lean; the n = 3 degree instantiations with the book's worked vocabularies in Studies/Bobaljik2012.lean.

Rules of exponence and derived specificity

structure Morphology.Containment.ExponenceRule (n : ℕ) (F : Type u_2) : Type u_2

A rule of exponence ([Bob12]'s term — Matthews's exponence, used in the realizational sense of [Stu01]) over an n-grade containment hierarchy. The rule realizes the initial span [0, spans] — the root when spans = 0, a root+heads portmanteau when spans > 0 — and applies only when the (optional) conditioning head context is present in the structure. DM vocabulary items are the Terminal-restricted special case; nanosyntax lexical entries share the context-free span format but pair it with Superset-based selection (Morphology/Containment/Superset.lean) rather than this file's containment-directed AppliesAt, so the insertion semantics differs. Latin ([Bob12] (204)): bon is ⟨bon, 0, none⟩, mel- is ⟨mel, 0, some 1⟩, the portmanteau opt- is ⟨opt, 1, some 2⟩.

• exponent : F

  The phonological exponent inserted for the span.

• spans : Fin n

  Upper end of the exponed initial span [0, spans].

• context : Option (Fin n)

  Head whose presence conditions the rule, if any.

@[implicit_reducible]

instance Morphology.Containment.instDecidableEqExponenceRule {n✝ : ℕ} {F✝ : Type u_2} [DecidableEq F✝] : DecidableEq (ExponenceRule n✝ F✝)

Equations

• Morphology.Containment.instDecidableEqExponenceRule = Morphology.Containment.instDecidableEqExponenceRule.decEq

def Morphology.Containment.instDecidableEqExponenceRule.decEq {n✝ : ℕ} {F✝ : Type u_2} [DecidableEq F✝] (x✝ x✝¹ : ExponenceRule n✝ F✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Morphology.Containment.instReprExponenceRule {n✝ : ℕ} {F✝ : Type u_2} [Repr F✝] : Repr (ExponenceRule n✝ F✝)

Equations

• Morphology.Containment.instReprExponenceRule = { reprPrec := Morphology.Containment.instReprExponenceRule.repr }

def Morphology.Containment.instReprExponenceRule.repr {n✝ : ℕ} {F✝ : Type u_2} [Repr F✝] : ExponenceRule n✝ F✝ → ℕ → Std.Format

Equations

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

def Morphology.Containment.ExponenceRule.threshold {n : ℕ} {F : Type u_1} (it : ExponenceRule n F) : Fin n

The least grade at which the rule is applicable: everything the rule mentions — exponed span and conditioning context — must be contained in the structure.

Equations

• it.threshold = max it.spans (it.context.getD it.spans)

def Morphology.Containment.ExponenceRule.AppliesAt {n : ℕ} {F : Type u_1} (it : ExponenceRule n F) (g : Fin n) : Prop

A rule applies at grade g when grade g's structure contains everything the rule mentions.

Equations

• it.AppliesAt g = (it.threshold ≤ g)

@[implicit_reducible]

instance Morphology.Containment.ExponenceRule.instDecidableAppliesAt {n : ℕ} {F : Type u_1} (it : ExponenceRule n F) (g : Fin n) : Decidable (it.AppliesAt g)

Equations

• it.instDecidableAppliesAt g = Morphology.Containment.ExponenceRule.instDecidableAppliesAt._aux_1 it g

theorem Morphology.Containment.ExponenceRule.appliesAt_iff {n : ℕ} {F : Type u_1} {it : ExponenceRule n F} {g : Fin n} : it.AppliesAt g ↔ it.spans ≤ g ∧ ∀ (c : Fin n), it.context = some c → c ≤ g

def Morphology.Containment.ExponenceRule.MoreSpecific {n : ℕ} {F : Type u_1} (it jt : ExponenceRule n F) : Prop

Pāṇinian specificity: it is at least as specific as jt when it applies in a subset of the structures jt applies in.

Equations

• it.MoreSpecific jt = ∀ ⦃g : Fin n⦄, it.AppliesAt g → jt.AppliesAt g

theorem Morphology.Containment.ExponenceRule.moreSpecific_iff_threshold_le {n : ℕ} {F : Type u_1} {it jt : ExponenceRule n F} : it.MoreSpecific jt ↔ jt.threshold ≤ it.threshold

Over a linear containment hierarchy, applicability sets are nested upward sets, so derived specificity is threshold comparison — the Elsewhere ordering ([Kip73]) is total and needs no stipulated specificity ranking.

Well-formedness conditions on vocabularies

Each generalization below hypothesizes exactly the conditions it needs; vocabularies violating a condition witness the corresponding unattested pattern (see the worked examples in Studies/Bobaljik2012.lean).

def Morphology.Containment.Terminal {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Prop

No portmanteaux: every rule expones the bare root.

Equations

• Morphology.Containment.Terminal v = ∀ it ∈ v, ↑it.spans = 0

@[implicit_reducible]

instance Morphology.Containment.instDecidableTerminal {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Decidable (Terminal v)

Equations

• Morphology.Containment.instDecidableTerminal v = id inferInstance

def Morphology.Containment.Adjacent {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Prop

Conditioning heads are adjacent to the exponed span — [Bob12]'s (tentatively adopted) adjacency condition on contextual allomorphy.

Equations

• Morphology.Containment.Adjacent v = ∀ it ∈ v, ∀ (c : Fin n), it.context = some c → ↑c = ↑it.spans + 1

@[implicit_reducible]

instance Morphology.Containment.instDecidableAdjacent {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Decidable (Adjacent v)

Equations

• Morphology.Containment.instDecidableAdjacent v = id inferInstance

def Morphology.Containment.Antihomophonous {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Prop

Distinct rules carry distinct exponents — [Bob12]'s Antihomophony assumption (44), closing the loophole of a surface-ABA pattern that is really an ABC with accidental A ≡ C homophony. Stated as pairwise antihomophony, a mild strengthening of the book's default-vs-contextual formulation; all worked vocabularies satisfy it.

Equations

• Morphology.Containment.Antihomophonous v = ∀ it ∈ v, ∀ jt ∈ v, it.exponent = jt.exponent → it = jt

@[implicit_reducible]

instance Morphology.Containment.instDecidableAntihomophonousOfDecidableEq {n : ℕ} {F : Type u_1} [DecidableEq F] (v : List (ExponenceRule n F)) : Decidable (Antihomophonous v)

Equations

• Morphology.Containment.instDecidableAntihomophonousOfDecidableEq v = id inferInstance

def Morphology.Containment.Grounded {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Prop

[Bob12]'s markedness condition (202): a context-sensitive rule of exponence involving a node requires a context-free rule involving that node. A rule is context-free for the node [0, k] when nothing it mentions extends beyond k — i.e. its threshold is k (the book's fn. 15 rewrites Latin mel- / __]CMPR] as the node-level context-free GOOD, CMPR → mel-CMPR) — so (202) says the vocabulary's threshold set is downward closed. On Adjacent vocabularies this is exactly the book's condition; on non-adjacent ones it is a mild strengthening (it also covers the skipped-head items the book independently excludes by adjacency).

Equations

• Morphology.Containment.Grounded v = ∀ it ∈ v, ∀ k < it.threshold, ∃ jt ∈ v, jt.threshold = k

@[implicit_reducible]

instance Morphology.Containment.instDecidableGrounded {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Decidable (Grounded v)

Equations

• Morphology.Containment.instDecidableGrounded v = id inferInstance

Elsewhere selection

def Morphology.Containment.applicable {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) (g : Fin n) : List (ExponenceRule n F)

The rules applicable at grade g, in vocabulary order.

Equations

• Morphology.Containment.applicable v g = List.filter (fun (it : Morphology.Containment.ExponenceRule n F) => decide (it.threshold ≤ g)) v

@[simp]

theorem Morphology.Containment.mem_applicable {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} {it : ExponenceRule n F} : it ∈ applicable v g ↔ it ∈ v ∧ it.threshold ≤ g

def Morphology.Containment.maxThreshold {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) (g : Fin n) : WithBot (Fin n)

The greatest applicable threshold at grade g — the specificity level of the Elsewhere winner, ⊥ when nothing applies.

Equations

• Morphology.Containment.maxThreshold v g = (List.map Morphology.Containment.ExponenceRule.threshold (Morphology.Containment.applicable v g)).maximum

theorem Morphology.Containment.maxThreshold_eq_bot_iff {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} : maxThreshold v g = ⊥ ↔ applicable v g = []

theorem Morphology.Containment.exists_of_maxThreshold_eq_coe {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) : ∃ it ∈ v, it.threshold = m ∧ m ≤ g

theorem Morphology.Containment.threshold_le_of_maxThreshold_eq_coe {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) {it : ExponenceRule n F} (hitv : it ∈ v) (hle : it.threshold ≤ g) : it.threshold ≤ m

theorem Morphology.Containment.maxThreshold_eq_coe_intro {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} {it : ExponenceRule n F} (hitv : it ∈ v) (hle : it.threshold ≤ g) (hub : ∀ jt ∈ v, jt.threshold ≤ g → jt.threshold ≤ it.threshold) : maxThreshold v g = ↑it.threshold

theorem Morphology.Containment.maxThreshold_eq_coe_of_between {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g g' m : Fin n} (h : maxThreshold v g' = ↑m) (hm : m ≤ g) (hg : g ≤ g') : maxThreshold v g = ↑m

The key transfer lemma: a winning threshold persists downward as long as it stays applicable. With monotone applicability this is what makes Elsewhere selection plateau between grades.

theorem Morphology.Containment.maxThreshold_eq_bot_of_le {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g g' : Fin n} (h : maxThreshold v g' = ⊥) (hg : g ≤ g') : maxThreshold v g = ⊥

def Morphology.Containment.winner {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) (g : Fin n) : Option (ExponenceRule n F)

The Elsewhere winner at grade g: the first rule attaining the greatest applicable threshold. By ExponenceRule.moreSpecific_iff_threshold_le, this is the most specific applicable rule.

Equations

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

theorem Morphology.Containment.winner_eq_none_of_bot {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} (h : maxThreshold v g = ⊥) : winner v g = none

theorem Morphology.Containment.winner_of_coe {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) : winner v g = List.find? (fun (it : ExponenceRule n F) => it.threshold == m) v

theorem Morphology.Containment.winner_spec {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} {it : ExponenceRule n F} (h : winner v g = some it) : it ∈ v ∧ maxThreshold v g = ↑it.threshold

theorem Morphology.Containment.exists_winner_of_coe {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) : ∃ (it : ExponenceRule n F), winner v g = some it

theorem Morphology.Containment.winner_eq_none_iff {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} : winner v g = none ↔ maxThreshold v g = ⊥

theorem Morphology.Containment.winner_congr {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g g' : Fin n} (h : maxThreshold v g = maxThreshold v g') : winner v g = winner v g'

def Morphology.Containment.realize {n : ℕ} {F : Type u_1} (v : List (ExponenceRule n F)) : Pattern n (Option F)

The realized pattern: at each grade, the Elsewhere winner's exponent (none when no rule applies — a paradigm gap).

Equations

• Morphology.Containment.realize v g = Option.map Morphology.Containment.ExponenceRule.exponent (Morphology.Containment.winner v g)

theorem Morphology.Containment.realize_congr {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g g' : Fin n} (h : maxThreshold v g = maxThreshold v g') : realize v g = realize v g'

theorem Morphology.Containment.realize_eq_none_iff {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} : realize v g = none ↔ maxThreshold v g = ⊥

CSG1: realization is contiguous

[Bob12] ch. 2: with antihomophonous rules, the Elsewhere competition over a containment hierarchy cannot generate ABA — with only two distinct listed root forms, no ordering of the rules yields an ABA pattern (p. 35). Formally: maxThreshold is the monotone score, the winner is a function of it, and antihomophony makes exponents injective in the winner — so realization factors as monotone-then-injective and Basic.lean's composition principle applies (here inlined as the sandwich argument).

theorem Morphology.Containment.isContiguous_realize {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} (hAH : Antihomophonous v) : IsContiguous (realize v)

The plateau: terminal adjacency generates only {AAA, ABB}

Capping all thresholds makes realization constant above the cap. With terminal rules and adjacent contexts the cap is the first head — this is the "Bobaljik-minus-portmanteaux" engine, which forces the comparative and superlative cells to coincide and so over-excludes the attested ABC patterns (Latin bon- mel- opt-). Portmanteau items (0 < spans) are what license ABC; see exists_portmanteau_of_ne.

theorem Morphology.Containment.applicable_eq_of_cap {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {m g g' : Fin n} (hcap : ∀ it ∈ v, it.threshold ≤ m) (hg : m ≤ g) (hg' : m ≤ g') : applicable v g = applicable v g'

theorem Morphology.Containment.realize_const_of_cap {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {m g g' : Fin n} (hcap : ∀ it ∈ v, it.threshold ≤ m) (hg : m ≤ g) (hg' : m ≤ g') : realize v g = realize v g'

theorem Morphology.Containment.realize_const_of_terminal_adjacent {F : Type u_1} {v : List (ExponenceRule 3 F)} (hT : Terminal v) (hA : Adjacent v) : realize v 1 = realize v 2

Terminal rules with adjacent contexts have thresholds at most the first head, so the comparative and superlative cells coincide: only AAA and ABB root patterns are generable.

Completeness: generable = contiguous

def Morphology.Containment.firstOcc {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) (g : Fin n) : Fin n

The earliest grade sharing g's form.

Equations

• Morphology.Containment.firstOcc p g = {j : Fin n | p j = p g}.min' ⋯

theorem Morphology.Containment.apply_firstOcc {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) (g : Fin n) : p (firstOcc p g) = p g

theorem Morphology.Containment.firstOcc_le {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) (g : Fin n) : firstOcc p g ≤ g

theorem Morphology.Containment.firstOcc_congr {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Pattern n F} {g g' : Fin n} (h : p g = p g') : firstOcc p g = firstOcc p g'

def Morphology.Containment.ofPattern {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) : List (ExponenceRule n F)

The canonical vocabulary of a pattern: one rule per form, introduced at the form's first grade and conditioned on it.

Equations

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

theorem Morphology.Containment.mem_ofPattern {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Pattern n F} {it : ExponenceRule n F} : it ∈ ofPattern p ↔ ∃ (s : Fin n), firstOcc p s = s ∧ it = { exponent := p s, spans := ⟨0, ⋯⟩, context := some s }

theorem Morphology.Containment.threshold_ofPattern {n : ℕ} {F : Type u_1} {p : Pattern n F} {s : Fin n} : { exponent := p s, spans := ⟨0, ⋯⟩, context := some s }.threshold = s

theorem Morphology.Containment.terminal_ofPattern {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) : Terminal (ofPattern p)

theorem Morphology.Containment.antihomophonous_ofPattern {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) : Antihomophonous (ofPattern p)

theorem Morphology.Containment.realize_ofPattern {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Pattern n F} (hp : IsContiguous p) (g : Fin n) : realize (ofPattern p) g = some (p g)

def Morphology.Containment.ElsewhereGenerable {n : ℕ} {F : Type u_1} (p : Pattern n F) : Prop

A pattern is Elsewhere-generable: some terminal antihomophonous vocabulary realizes it in full.

Equations

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

theorem Morphology.Containment.isContiguous_iff_generable {n : ℕ} {F : Type u_1} (p : Pattern n F) : IsContiguous p ↔ ElsewhereGenerable p

Generable = contiguous. A fully realized pattern arises from Elsewhere insertion over a terminal antihomophonous vocabulary iff it is contiguous: the forward direction is the canonical-vocabulary construction, the backward direction CSG1.

Three-grade hierarchies: *AAB and the portmanteau prediction

theorem Morphology.Containment.csg2 {F : Type u_1} {v : List (ExponenceRule 3 F)} (hAH : Antihomophonous v) (hG : Grounded v) (h01 : realize v 0 = realize v 1) (h2 : (realize v 2).isSome = true) : realize v 1 = realize v 2

*CSG2 / AAB exclusion ([Bob12] ch. 5). Over the three-grade degree hierarchy, if the positive and comparative cells agree and the superlative cell is realized, all three agree: good – gooder – *best is not generable. Hypotheses: antihomophony plus Grounded (the book's markedness condition (202)); the threshold-set downward closure makes both of the book's AAB routes — the skipped-head root rule (190a) and the context-sensitive portmanteau (201) — fail for the same reason, a threshold gap at the comparative grade.

theorem Morphology.Containment.exists_portmanteau_of_ne {F : Type u_1} {v : List (ExponenceRule 3 F)} (hA : Adjacent v) (h12 : realize v 1 ≠ realize v 2) : ∃ it ∈ v, winner v 2 = some it ∧ 0 < ↑it.spans

ABC requires a portmanteau ([Bob12] §5.3.1, the degree-domain consequence generalized there as (199)): under adjacency, root allomorphy at the superlative grade distinct from the comparative grade arises only via a portmanteau — the winning rule must expone more than the bare root (Latin opt-, Welsh gor-).