Containment hierarchies: contiguity and the suppletion generalizations

The *ABA generalization and its refinements, over the score selection of Containment/Selection.lean. Both engines are *ABA-free (isContiguous_realize, isContiguous_spellout), generate exactly the contiguous patterns (isContiguous_iff_generable, isContiguous_iff_spelloutGenerable), and are equigenerative on total realizations (spelloutGenerable_iff_generable). The DM-specific refinements — the terminal-adjacent plateau, *AAB exclusion (realize_const_of_grounded), and the ABC portmanteau prediction (exists_portmanteau_of_ne) — follow from the plateau lemmas of maxThreshold.

Main declarations

• isContiguous_realize, isContiguous_spellout — *ABA for both readings
• isContiguous_iff_generable, isContiguous_iff_spelloutGenerable — generable = spellable = contiguous
• spelloutGenerable_iff_generable — DM/nanosyntax equigenerativity
• realize_const_of_terminal_adjacent, realize_const_of_grounded, exists_portmanteau_of_ne — the plateau, *AAB, and portmanteau prediction

*ABA for Elsewhere insertion

[Bob12] ch. 2: with antihomophonous rules, the Elsewhere competition over a containment hierarchy cannot generate ABA. 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.

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

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

theorem Morphology.Containment.applicable_eq_of_cap {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule 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 (SpanRule 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 : Paradigm 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 : Paradigm n F) (g : Fin n) : p (firstOcc p g) = p g

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

theorem Morphology.Containment.firstOcc_congr {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Paradigm 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 : Paradigm n F) : List (SpanRule 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 : Paradigm n F} {it : SpanRule 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 : Paradigm 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 : Paradigm n F) : Terminal (ofPattern p)

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

theorem Morphology.Containment.realize_ofPattern {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Paradigm 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 : Paradigm 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 : Paradigm 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.realize_const_of_grounded {F : Type u_1} {v : List (SpanRule 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 — given antihomophony and Grounded (the book's condition (202)).

theorem Morphology.Containment.exists_portmanteau_of_ne {F : Type u_1} {v : List (SpanRule 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-).

*ABA for Superset spellout

The mirror image of isContiguous_realize: minSpan is monotone in the grade, the winner is a function of it, and antihomophony makes the winner's exponent injective — so spellout fibers are convex ([Cah09]).

theorem Morphology.Containment.isContiguous_spellout {n : ℕ} {F : Type u_1} {v : List (SpanRule n F)} (hAH : Antihomophonous v) : IsContiguous (spellout v)

Completeness: spellable = contiguous

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

The latest grade sharing g's form.

Equations

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

theorem Morphology.Containment.apply_lastOcc {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Paradigm n F) (g : Fin n) : p (lastOcc p g) = p g

theorem Morphology.Containment.le_lastOcc {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Paradigm n F) (g : Fin n) : g ≤ lastOcc p g

theorem Morphology.Containment.lastOcc_congr {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Paradigm n F} {g g' : Fin n} (h : p g = p g') : lastOcc p g = lastOcc p g'

def Morphology.Containment.spelloutOfPattern {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Paradigm n F) : List (SpanRule n F)

The canonical nanosyntax lexicon of a pattern: one context-free entry per form, storing the form's largest constituent.

Equations

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

theorem Morphology.Containment.mem_spelloutOfPattern {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Paradigm n F} {it : SpanRule n F} : it ∈ spelloutOfPattern p ↔ ∃ (s : Fin n), lastOcc p s = s ∧ it = { exponent := p s, spans := s, context := none }

theorem Morphology.Containment.contextFree_spelloutOfPattern {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Paradigm n F) : ContextFree (spelloutOfPattern p)

theorem Morphology.Containment.antihomophonous_spelloutOfPattern {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Paradigm n F) : Antihomophonous (spelloutOfPattern p)

theorem Morphology.Containment.spellout_spelloutOfPattern {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Paradigm n F} (hp : IsContiguous p) (g : Fin n) : spellout (spelloutOfPattern p) g = some (p g)

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

A pattern is Superset-spellable: some context-free antihomophonous lexicon spells it out in full.

Equations

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

theorem Morphology.Containment.isContiguous_iff_spelloutGenerable {n : ℕ} {F : Type u_1} (p : Paradigm n F) : IsContiguous p ↔ SupersetSpellable p

Spellable = contiguous: a fully realized pattern arises from Superset spellout over a context-free antihomophonous lexicon iff it is contiguous — [Cah09]'s Universal Contiguity as a theorem of the engine; the converse sharpens it to exact generative capacity.

theorem Morphology.Containment.spelloutGenerable_iff_generable {n : ℕ} {F : Type u_1} (p : Paradigm n F) : SupersetSpellable p ↔ ElsewhereGenerable p

DM and nanosyntax are equigenerative over linear containment hierarchies: Superset spellout from context-free antihomophonous lexicons and Elsewhere insertion from terminal antihomophonous vocabularies generate exactly the same fully realized patterns — the contiguous ones. The frameworks differ intensionally (rule format and selection direction) but not in generative capacity on this fragment.

Where the frameworks diverge

On partial lexicons the selection directions come apart: an overspecified entry realizes smaller structures under the Superset Principle but leaves a gap under Elsewhere insertion — nanosyntax's characteristic prediction ([DCVW17]) against DM's characteristic gaps.

Antihomophony is necessary for *ABA

Two distinct entries sharing an exponent — accidental homophony, an Antihomophonous violation — generate ABA. [Cah09] distinguishes accidental homophony (phonological) from systematic syncretism (one item over a contiguous span); the Antihomophonous hypothesis is that distinction.