Superset spellout over containment hierarchies

[Sta09a] [Cah09] [Bob12]

The static core of the nanosyntax selection rule (no cyclic override or spellout-driven movement), stated over the same ExponenceRule vocabularies as the Elsewhere engine of Morphology/Containment/Vocabulary.lean. A nanosyntax lexical entry stores a constituent and carries no contextual restriction (ContextFree); it can spell out any structure it contains — the Superset Principle ([Sta09a]) — and competition selects the smallest matching entry (Minimize Junk, which [Sta09a] himself identifies with the Elsewhere Condition: the directional asymmetry lives in the matching relation, not in the competition). The two engines are dual: Elsewhere insertion maximizes the threshold over rules the structure contains; Superset spellout minimizes the span over entries that contain the structure.

The headline is the cross-framework theorem spelloutGenerable_iff_generable: over a linear containment hierarchy, Superset spellout from context-free antihomophonous entries and Elsewhere insertion from terminal antihomophonous rules generate exactly the same fully-realized patterns — the contiguous ones. The frameworks are extensionally equivalent on this fragment while differing intensionally: an overspecified entry realizes smaller structures under Superset but yields a gap under Elsewhere insertion (see the divergence examples at the end), which is how nanosyntax derives ABC with no contextual apparatus — suppletion as pure phrasal spellout, portmanteau by constituent size with no environment restriction ([DCVW17] for exactly this Latin degree case) — where DM needs the context-restricted portmanteau of [Bob12] ch. 5.

Main declarations

• ExponenceRule.Matches — the Superset Principle: entry contains the target structure
• ContextFree — the nanosyntax restriction on vocabularies
• minSpan, spelloutWinner, spellout — Minimize-Junk competition and the realized pattern
• isContiguous_spellout — *ABA for Superset spellout
• isContiguous_iff_spelloutGenerable — spellable = contiguous
• spelloutGenerable_iff_generable — DM/nanosyntax equigenerativity

The older tree-based nanosyntax fragment (Morphology/Nanosyntax/Basic.lean) predates this engine and is not yet grounded in it.

The Superset Principle

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

The Superset Principle ([Sta09a]): an entry can spell out grade g when the constituent it stores contains grade g's structure. Anti-monotone in g, dually to AppliesAt.

Equations

• it.Matches g = (g ≤ it.spans)

@[implicit_reducible]

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

Equations

• Morphology.Containment.instDecidableMatches it g = Morphology.Containment.instDecidableMatches._aux_1 it g

theorem Morphology.Containment.ExponenceRule.Matches.anti {n : ℕ} {F : Type u_1} {it : ExponenceRule n F} {g g' : Fin n} (h : it.Matches g') (hg : g ≤ g') : it.Matches g

theorem Morphology.Containment.ExponenceRule.matches_imp_iff_spans_le {n : ℕ} {F : Type u_1} {it jt : ExponenceRule n F} : (∀ ⦃g : Fin n⦄, it.Matches g → jt.Matches g) ↔ it.spans ≤ jt.spans

Minimize Junk derived, dually to ExponenceRule.moreSpecific_iff_threshold_le: an entry matches in a subset of the structures another matches in iff it stores the smaller constituent — smallest-match selection is Pāṇinian specificity under superset matching.

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

The nanosyntax restriction, in the pointer-free idealization of [Cah09]: entries store bare constituents, with no DM-style contextual environment.

Equations

• Morphology.Containment.ContextFree v = ∀ it ∈ v, it.context = none

@[implicit_reducible]

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

Equations

• Morphology.Containment.instDecidableContextFree v = id inferInstance

Minimize-Junk competition

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

The entries matching at grade g, in vocabulary order.

Equations

• Morphology.Containment.matching v g = List.filter (fun (it : Morphology.Containment.ExponenceRule n F) => decide (it.Matches g)) v

@[simp]

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

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

The least matching span at grade g — Minimize Junk: the winning entry stores as little unrealized structure as possible. ⊤ when no entry matches.

Equations

• Morphology.Containment.minSpan v g = (List.map Morphology.Containment.ExponenceRule.spans (Morphology.Containment.matching v g)).minimum

theorem Morphology.Containment.minSpan_eq_top_iff {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} : minSpan v g = ⊤ ↔ matching v g = []

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

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

theorem Morphology.Containment.minSpan_eq_coe_intro {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} {it : ExponenceRule n F} (hitv : it ∈ v) (hle : g ≤ it.spans) (hlb : ∀ jt ∈ v, g ≤ jt.spans → it.spans ≤ jt.spans) : minSpan v g = ↑it.spans

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

The key transfer lemma, dual to maxThreshold_eq_coe_of_le: a winning span persists upward as long as the grade stays inside it.

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

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

The spellout winner at grade g: the first entry attaining the least matching span.

Equations

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

theorem Morphology.Containment.spelloutWinner_eq_none_of_top {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} (h : minSpan v g = ⊤) : spelloutWinner v g = none

theorem Morphology.Containment.spelloutWinner_of_coe {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g m : Fin n} (h : minSpan v g = ↑m) : spelloutWinner v g = List.find? (fun (it : ExponenceRule n F) => it.spans == m) v

theorem Morphology.Containment.spelloutWinner_spec {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} {it : ExponenceRule n F} (h : spelloutWinner v g = some it) : it ∈ v ∧ minSpan v g = ↑it.spans

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

theorem Morphology.Containment.spelloutWinner_eq_none_iff {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} : spelloutWinner v g = none ↔ minSpan v g = ⊤

theorem Morphology.Containment.spelloutWinner_congr {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g g' : Fin n} (h : minSpan v g = minSpan v g') : spelloutWinner v g = spelloutWinner v g'

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

The spelled-out pattern: at each grade, the Minimize-Junk winner's exponent (none when no entry contains the structure — a spellout gap; full nanosyntax would attempt rescue operations before declaring ineffability).

Equations

• Morphology.Containment.spellout v g = Option.map Morphology.Containment.ExponenceRule.exponent (Morphology.Containment.spelloutWinner v g)

theorem Morphology.Containment.spellout_congr {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g g' : Fin n} (h : minSpan v g = minSpan v g') : spellout v g = spellout v g'

theorem Morphology.Containment.spellout_eq_none_iff {n : ℕ} {F : Type u_1} {v : List (ExponenceRule n F)} {g : Fin n} : spellout v g = none ↔ minSpan v g = ⊤

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

Spellout gaps propagate upward: an entry matching a higher grade would match the lower one too, so a gap at g forces gaps at every g' ≥ g — [Dek21]'s paradigm-gap monotonicity for indefinites.

*ABA for Superset spellout

The mirror image of isContiguous_realize: minSpan is monotone in the grade (matching sets shrink upward, so the least span weakly grows), the winner is a function of it, and antihomophony makes the winner's exponent injective — so spellout fibers are convex. This is the nanosyntax derivation of *ABA ([Cah09]), run on the same vocabulary type as the DM derivation.

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

Completeness: spellable = contiguous

def Morphology.Containment.lastOcc {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern 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 : Pattern n F) (g : Fin n) : p (lastOcc p g) = p g

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

theorem Morphology.Containment.lastOcc_congr {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Pattern 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 : Pattern n F) : List (ExponenceRule 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 : Pattern n F} {it : ExponenceRule 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 : Pattern n F) : ContextFree (spelloutOfPattern p)

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

theorem Morphology.Containment.spellout_spelloutOfPattern {n : ℕ} {F : Type u_1} [DecidableEq F] {p : Pattern 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 : Pattern 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 : Pattern 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, mirroring Caha's own derivation of UC from the Superset Principle; the converse direction sharpens it to exact generative capacity.

theorem Morphology.Containment.spelloutGenerable_iff_generable {n : ℕ} {F : Type u_1} (p : Pattern 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; see the divergence examples below) but not in generative capacity on this fragment.

Where the frameworks diverge

The equivalence is extensional, over total realizations. 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. This is nanosyntax's characteristic prediction — overspecified entries double as defaults for smaller structures — against DM's characteristic gaps.

Antihomophony is necessary for *ABA

Two distinct entries sharing an exponent — accidental homophony, an Antihomophonous violation — generate ABA: with "A" stored at grades 0 and 2 and "B" at grade 1, Minimize Junk yields A–B–A. [Cah09] distinguishes accidental homophony (phonological) from systematic syncretism (one item over a contiguous span); the Antihomophonous hypothesis of isContiguous_spellout is exactly that distinction.