Containment hierarchies: score selection

Elsewhere insertion and Superset spellout. The DM winner maximizes threshold as an instantiation of the core's Exponence.selectBy, so winner_isElsewhereWinner is an instance of selectBy_isElsewhereWinner discharged by moreSpecific_iff_threshold_le. The nanosyntax spelloutWinner minimizes spans; its SupersetRule carrier is a semireducible synonym that does not sit cleanly under selectBy, so it runs on SpanRule directly and spelloutWinner_isElsewhereWinner transports the result onto the core's Superset reading. maxThreshold and minSpan are the score aggregates the plateau theorems (Containment/Contiguity.lean) reason about — contexts and scores share Fin n.

Main declarations

• winner, realize — Elsewhere selection and the realized pattern
• spelloutWinner, spellout — Minimize-Junk selection and the spelled pattern
• winner_isElsewhereWinner, spelloutWinner_isElsewhereWinner — both are Elsewhere winners of the shared core
• maxThreshold, minSpan — the score aggregates, with their transfer lemmas

General list helpers

Subset reading: Elsewhere selection

@[reducible, inline]

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

The rules applicable at grade g, in vocabulary order.

Equations

• Morphology.Containment.applicable v g = Morphology.Exponence.applicable v g

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

def Morphology.Containment.maxThreshold {n : ℕ} {F : Type u_1} (v : List (SpanRule 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.SpanRule.threshold (Morphology.Containment.applicable v g)).maximum

theorem Morphology.Containment.maxThreshold_eq_bot_iff {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule 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 (SpanRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) {it : SpanRule 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 (SpanRule n F)} {g : Fin n} {it : SpanRule 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 (SpanRule n F)} {g g' m : Fin n} (h : maxThreshold v g' = ↑m) (hm : m ≤ g) (hg : g ≤ g') : maxThreshold v g = ↑m

A winning threshold persists downward as long as it stays applicable, which is what makes Elsewhere selection plateau between grades.

theorem Morphology.Containment.maxThreshold_eq_bot_of_le {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule n F)) (g : Fin n) : Option (SpanRule n F)

The Elsewhere winner at grade g: the applicable rule with greatest threshold — the most specific applicable rule — as Exponence.selectBy.

Equations

• Morphology.Containment.winner v g = Morphology.Exponence.selectBy Morphology.Containment.SpanRule.threshold v g

theorem Morphology.Containment.winner_eq_none_of_bot {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) : winner v g = List.find? (fun (it : SpanRule n F) => it.threshold == m) v

theorem Morphology.Containment.winner_spec {n : ℕ} {F : Type u_1} {v : List (SpanRule n F)} {g : Fin n} {it : SpanRule 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 (SpanRule n F)} {g m : Fin n} (h : maxThreshold v g = ↑m) : ∃ (it : SpanRule n F), winner v g = some it

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

theorem Morphology.Containment.winner_congr {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule n F)) : Paradigm n (Option F)

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

Equations

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

theorem Morphology.Containment.realize_congr {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule n F)} {g : Fin n} : realize v g = none ↔ maxThreshold v g = ⊥

theorem Morphology.Containment.winner_isElsewhereWinner {n : ℕ} {F : Type u_1} {v : List (SpanRule n F)} {g : Fin n} {it : SpanRule n F} (h : winner v g = some it) : Exponence.IsElsewhereWinner v g it

The containment engine's Elsewhere winner is an Elsewhere winner of the shared core — an instance of selectBy_isElsewhereWinner.

Superset reading: Minimize-Junk selection

The dual engine, on the SupersetRule reading. The nanosyntax lexical entry stores a constituent and can spell out any structure it contains, with competition selecting the smallest matching entry (Minimize Junk). spelloutWinner selects by least matching span; minSpan is the score aggregate the completeness lemmas reason about. The SupersetRule carrier is a semireducible synonym, so the selection here runs directly on SpanRule; spelloutWinner_isElsewhereWinner transports the result onto the superset reading of the shared core.

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

The entries matching at grade g, in vocabulary order.

Equations

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

@[simp]

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

def Morphology.Containment.minSpan {n : ℕ} {F : Type u_1} (v : List (SpanRule 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.SpanRule.spans (Morphology.Containment.matching v g)).minimum

theorem Morphology.Containment.minSpan_eq_top_iff {n : ℕ} {F : Type u_1} {v : List (SpanRule 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 (SpanRule 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 (SpanRule n F)} {g m : Fin n} (h : minSpan v g = ↑m) {it : SpanRule 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 (SpanRule n F)} {g : Fin n} {it : SpanRule 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 (SpanRule 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_between: 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 (SpanRule 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 (SpanRule n F)) (g : Fin n) : Option (SpanRule 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 (SpanRule 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 (SpanRule n F)} {g m : Fin n} (h : minSpan v g = ↑m) : spelloutWinner v g = List.find? (fun (it : SpanRule n F) => it.spans == m) v

theorem Morphology.Containment.spelloutWinner_spec {n : ℕ} {F : Type u_1} {v : List (SpanRule n F)} {g : Fin n} {it : SpanRule 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 (SpanRule n F)} {g m : Fin n} (h : minSpan v g = ↑m) : ∃ (it : SpanRule n F), spelloutWinner v g = some it

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

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

Equations

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

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

theorem Morphology.Containment.spelloutWinner_isElsewhereWinner {n : ℕ} {F : Type u_1} {v : List (SpanRule n F)} {g : Fin n} {it : SpanRule n F} (h : spelloutWinner v g = some it) : Exponence.IsElsewhereWinner (List.map SpanRule.superset v) g it.superset

Minimize-Junk selection is an Elsewhere winner of the shared core under the Superset reading — with no side conditions: over a linear hierarchy the span order is total, so the least-span match is maximally specific.

The chain decomposition: containment as feature decomposition

The linear containment engine is the chain instance of the general feature-decomposition engine (Exponence/Decomposition.lean): decompose the grade space Fin n by initial segments chainDecomp i = Finset.Iic i, and a span rule realizing [0, threshold] becomes a decomposition rule specified for exactly those features. Threshold containment is then Subset containment (applies_toDecomposition), the specificity orders correspond (SpanRule.toDecomposition_le_iff), and the Elsewhere winner selected by maximizing threshold is the same rule the decomposition engine selects by maximizing feats.card = threshold + 1 — an Elsewhere winner of the shared core under the decomposition reading (winner_isElsewhereWinner_toDecomposition).

def Morphology.Containment.chainDecomp {n : ℕ} : Fin n → Finset (Fin n)

The chain decomposition of an n-grade hierarchy: grade i carries the initial segment [0, i].

Equations

• Morphology.Containment.chainDecomp = Finset.Iic

def Morphology.Containment.SpanRule.toDecomposition {n : ℕ} {F : Type u_1} (it : SpanRule n F) : Decomposition.Rule (Fin n) chainDecomp F

A span rule read as a feature-decomposition rule over chainDecomp: its threshold becomes the initial-segment feature set [0, threshold], the exponent unchanged.

Equations

• it.toDecomposition = { feats := Finset.Iic it.threshold, exponent := it.exponent }

@[simp]

theorem Morphology.Containment.SpanRule.toDecomposition_feats {n : ℕ} {F : Type u_1} {it : SpanRule n F} : it.toDecomposition.feats = Finset.Iic it.threshold

@[simp]

theorem Morphology.Containment.applies_toDecomposition {n : ℕ} {F : Type u_1} {it : SpanRule n F} {g : Fin n} : Exponence.Applies it.toDecomposition g ↔ Exponence.Applies it g

Applicability agreement: threshold containment is Subset containment of initial segments.

theorem Morphology.Containment.SpanRule.toDecomposition_feats_card {n : ℕ} {F : Type u_1} {it : SpanRule n F} : it.toDecomposition.feats.card = ↑it.threshold + 1

The feature count of a chain rule is one more than its threshold, so feats.card-maximization is threshold-maximization: the two engines optimize the same score.

theorem Morphology.Containment.SpanRule.toDecomposition_le_iff {n : ℕ} {F : Type u_1} {it jt : SpanRule n F} : it.toDecomposition ≤ jt.toDecomposition ↔ it ≤ jt

Specificity agreement: the chain map reflects the specificity preorder — it is at least as specific as jt under the linear threshold order iff its decomposition image is under Subset inclusion.

theorem Morphology.Containment.winner_isElsewhereWinner_toDecomposition {n : ℕ} {F : Type u_1} {v : List (SpanRule n F)} {g : Fin n} {it : SpanRule n F} (h : winner v g = some it) : Exponence.IsElsewhereWinner (List.map SpanRule.toDecomposition v) g it.toDecomposition

Winner agreement: the containment Elsewhere winner, read through the chain map, is an Elsewhere winner of the shared core under the decomposition reading — so Containment.winner (maximizing threshold) and Decomposition.pattern (selectBy feats.card) pick the same rule.