Nanosyntax: Tree-Based Spellout

Extension of rank-based Superset spellout (Morphology/Exponence/Containment/Contiguity.lean) to tree-structured spellout. Implements the Superset Principle (SP) for trees: a lexical entry M ↔ S' can spell out syntactic target S if S' structurally contains S (NanoTree.Contains). Among matching entries, the Elsewhere Condition selects the smallest (by tree size).

The SP on trees is a consequence of [Sta09a]'s Matching relation (formalized in [TTML18] as (35)): M matches S iff there exists a node N in M's stored tree such that S and N have the same root label and mutually matching daughters. For the right-branching single-daughter trees used in Bantu class prefix analysis, structural containment and bidirectional Matching coincide; the implementation uses containment as the simpler equivalent formulation.

Main declarations

• NanoTree: feature trees; NanoTree.Contains: sub-constituency
• TreeLexEntry: a stored tree paired with an exponent; TreeLexEntry.Matches
• treeSelect, treeSpellout: Superset Principle + Elsewhere Condition
• treeSelect_isElsewhereWinner: the engine as an instance of the shared exponence core (Exponence) — derived specificity is reverse tree containment (TreeLexEntry.le_iff), and smallest-tree selection is an Elsewhere winner with no side conditions
• FootConditionMet: [TTML18]'s constraint on backtracking
• chain_contains_iff_le: for right-branching chains, tree containment reduces to rank comparison — tree-based spellout generalizes (not replaces) rank-based spellout

inductive Morphology.Nanosyntax.MorphType : Type

Morphological type of an exponent derived from nanosyntactic spellout. Suffixes arise from spellout-driven movement (roll-up, unary foot); prefixes arise from subderivation (binary foot) — [Dek21] for this diagnostic on indefinite markers.

• suffix : MorphType
• prefix : MorphType

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableEqMorphType : DecidableEq MorphType

Equations

• Morphology.Nanosyntax.instDecidableEqMorphType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Nanosyntax.instReprMorphType.repr : MorphType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Nanosyntax.instReprMorphType : Repr MorphType

Equations

• Morphology.Nanosyntax.instReprMorphType = { reprPrec := Morphology.Nanosyntax.instReprMorphType.repr }

NanoTree

inductive Morphology.Nanosyntax.NanoTree (F : Type u_1) : Type u_1

A nanosyntactic feature tree. Simpler than Syntax — no traces, no binding, no category/word split. Just labeled nodes with an ordered list of daughters.

leaf f = a terminal feature. node f children = feature f dominating daughters.

• leaf {F : Type u_1} : F → NanoTree F
• node {F : Type u_1} : F → List (NanoTree F) → NanoTree F

partial def Morphology.Nanosyntax.instReprNanoTree.repr {F✝ : Type u_1} [Repr F✝] : NanoTree F✝ → ℕ → Std.Format

@[instance_reducible]

instance Morphology.Nanosyntax.instReprNanoTree {F✝ : Type u_1} [Repr F✝] : Repr (NanoTree F✝)

Equations

• Morphology.Nanosyntax.instReprNanoTree = { reprPrec := Morphology.Nanosyntax.instReprNanoTree.repr }

Decidable equality

Defined by structural recursion (not deriving DecidableEq, which routes the nested List through well-founded recursion and does not kernel-reduce; decide-style spellout evaluations need the structural form).

def Morphology.Nanosyntax.NanoTree.decEq {F : Type u_1} [DecidableEq F] (s t : NanoTree F) : Decidable (s = t)

Structural decidable equality on trees.

Equations

• One or more equations did not get rendered due to their size.
• (Morphology.Nanosyntax.NanoTree.leaf f).decEq (Morphology.Nanosyntax.NanoTree.leaf g) = if h : f = g then isTrue ⋯ else isFalse ⋯
• (Morphology.Nanosyntax.NanoTree.leaf a).decEq (Morphology.Nanosyntax.NanoTree.node a_1 a_2) = isFalse ⋯
• (Morphology.Nanosyntax.NanoTree.node a a_1).decEq (Morphology.Nanosyntax.NanoTree.leaf a_2) = isFalse ⋯

def Morphology.Nanosyntax.NanoTree.decEq.decEqList {F : Type u_1} [DecidableEq F] (cs ds : List (NanoTree F)) : Decidable (cs = ds)

Structural decidable equality on daughter lists.

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Nanosyntax.NanoTree.decEq.decEqList [] [] = isTrue ⋯
• Morphology.Nanosyntax.NanoTree.decEq.decEqList [] (head :: tail) = isFalse ⋯
• Morphology.Nanosyntax.NanoTree.decEq.decEqList (head :: tail) [] = isFalse ⋯

@[instance_reducible]

instance Morphology.Nanosyntax.NanoTree.instDecidableEq {F : Type u_1} [DecidableEq F] : DecidableEq (NanoTree F)

Equations

• Morphology.Nanosyntax.NanoTree.instDecidableEq = Morphology.Nanosyntax.NanoTree.decEq

Size

def Morphology.Nanosyntax.NanoTree.size {F : Type u_1} : NanoTree F → ℕ

Number of nodes in the tree. Used by the Elsewhere Condition to select the smallest matching entry.

Equations

• (Morphology.Nanosyntax.NanoTree.leaf a).size = 1
• (Morphology.Nanosyntax.NanoTree.node a a_1).size = 1 + Morphology.Nanosyntax.NanoTree.size.sizeList a_1

def Morphology.Nanosyntax.NanoTree.size.sizeList {F : Type u_1} : List (NanoTree F) → ℕ

Equations

• Morphology.Nanosyntax.NanoTree.size.sizeList [] = 0
• Morphology.Nanosyntax.NanoTree.size.sizeList (t :: ts) = t.size + Morphology.Nanosyntax.NanoTree.size.sizeList ts

Containment (Superset Principle on trees)

inductive Morphology.Nanosyntax.NanoTree.Contains {F : Type u_1} : NanoTree F → NanoTree F → Prop

Contains self target: target occurs in self as a sub-constituent. Implements the tree-generalized Superset Principle ([Cah09] §2.2, [TTML18] (36)): entry M matches target S if M's stored tree contains S.

For right-branching single-daughter trees (all Bantu class prefix structures), this is equivalent to the bidirectional Matching relation ([TTML18] (35)).

For 1D chains: a chain of depth n contains all chains of depth k ≤ n, matching SpanRule.Matches (chain_contains_iff_le).

• refl {F : Type u_1} (t : NanoTree F) : t.Contains t
• child {F : Type u_1} {f : F} {cs : List (NanoTree F)} {c target : NanoTree F} : c ∈ cs → c.Contains target → (node f cs).Contains target

@[simp]

theorem Morphology.Nanosyntax.NanoTree.contains_leaf_iff {F : Type u_1} {f : F} {t : NanoTree F} : (leaf f).Contains t ↔ leaf f = t

theorem Morphology.Nanosyntax.NanoTree.contains_node_iff {F : Type u_1} {f : F} {cs : List (NanoTree F)} {t : NanoTree F} : (node f cs).Contains t ↔ node f cs = t ∨ ∃ c ∈ cs, c.Contains t

def Morphology.Nanosyntax.NanoTree.decContains {F : Type u_1} [DecidableEq F] (s t : NanoTree F) : Decidable (s.Contains t)

Structural decision procedure for containment (kernel-reducible).

Equations

• One or more equations did not get rendered due to their size.
• (Morphology.Nanosyntax.NanoTree.leaf f).decContains x✝ = if h : Morphology.Nanosyntax.NanoTree.leaf f = x✝ then isTrue ⋯ else isFalse ⋯

def Morphology.Nanosyntax.NanoTree.decContains.decAny {F : Type u_1} [DecidableEq F] (cs : List (NanoTree F)) (t : NanoTree F) : Decidable (∃ c ∈ cs, c.Contains t)

Does some member of cs contain t?

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Nanosyntax.NanoTree.decContains.decAny [] t = isFalse ⋯

@[instance_reducible]

instance Morphology.Nanosyntax.NanoTree.instDecidableContainsOfDecidableEq {F : Type u_1} [DecidableEq F] (s t : NanoTree F) : Decidable (s.Contains t)

Equations

• s.instDecidableContainsOfDecidableEq t = s.decContains t

theorem Morphology.Nanosyntax.NanoTree.Contains.trans {F : Type u_1} {a b c : NanoTree F} (h₁ : a.Contains b) (h₂ : b.Contains c) : a.Contains c

@[instance_reducible]

instance Morphology.Nanosyntax.NanoTree.instTransContains {F : Type u_1} : Trans Contains Contains Contains

Equations

• Morphology.Nanosyntax.NanoTree.instTransContains = { trans := ⋯ }

theorem Morphology.Nanosyntax.NanoTree.le_sizeList_of_mem {F : Type u_1} {cs : List (NanoTree F)} {c : NanoTree F} (h : c ∈ cs) : c.size ≤ size.sizeList cs

Each daughter's size is bounded by the daughters' total size.

theorem Morphology.Nanosyntax.NanoTree.size_lt_of_mem {F : Type u_1} {f : F} {cs : List (NanoTree F)} {c : NanoTree F} (h : c ∈ cs) : c.size < (node f cs).size

theorem Morphology.Nanosyntax.NanoTree.Contains.size_le {F : Type u_1} {s t : NanoTree F} (h : s.Contains t) : t.size ≤ s.size

Containment is size-monotone: a contained tree is no larger.

theorem Morphology.Nanosyntax.NanoTree.Contains.eq_of_size_le {F : Type u_1} {s t : NanoTree F} (h : s.Contains t) (hs : s.size ≤ t.size) : s = t

Containment is size-strict off the diagonal: a contained tree of no smaller size is the tree itself.

theorem Morphology.Nanosyntax.NanoTree.Contains.antisymm {F : Type u_1} {s t : NanoTree F} (h₁ : s.Contains t) (h₂ : t.Contains s) : s = t

Foot

def Morphology.Nanosyntax.NanoTree.foot {F : Type u_1} : NanoTree F → F

The foot of a tree: the feature at the bottom of the leftmost spine. For right-branching chains [Fn [... [F0]]], the foot is F0 — the deepest feature on the functional sequence.

Equations

• (Morphology.Nanosyntax.NanoTree.leaf f).foot = f
• (Morphology.Nanosyntax.NanoTree.node f []).foot = f
• (Morphology.Nanosyntax.NanoTree.node a (child :: tail)).foot = child.foot

Tree lexical entry

structure Morphology.Nanosyntax.TreeLexEntry (F : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A nanosyntactic lexical entry storing a tree rather than a scalar rank, paired with an exponent of type α (String in concrete fragments). The tree encodes the full feature geometry that the morpheme lexicalizes.

Contrast with SpanRule (Morphology/Exponence/Containment/Contiguity.lean) which stores only a span (depth on a 1D functional sequence).

• tree : NanoTree F

  The stored feature tree.

• exponent : α

  The exponent.

• morphType : MorphType

  Morphological type (suffix or prefix).

@[instance_reducible]

instance Morphology.Nanosyntax.instReprTreeLexEntry {F✝ : Type u_1} {α✝ : Type u_2} [Repr F✝] [Repr α✝] : Repr (TreeLexEntry F✝ α✝)

Equations

• Morphology.Nanosyntax.instReprTreeLexEntry = { reprPrec := Morphology.Nanosyntax.instReprTreeLexEntry.repr }

def Morphology.Nanosyntax.instReprTreeLexEntry.repr {F✝ : Type u_1} {α✝ : Type u_2} [Repr F✝] [Repr α✝] : TreeLexEntry F✝ α✝ → ℕ → Std.Format

Equations

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

def Morphology.Nanosyntax.TreeLexEntry.Matches {F : Type u_1} {α : Type u_2} (entry : TreeLexEntry F α) (target : NanoTree F) : Prop

A tree-based entry matches a target under the Superset Principle iff its stored tree contains the target as a sub-constituent.

Equations

• entry.Matches target = entry.tree.Contains target

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq {F : Type u_1} {α : Type u_2} [DecidableEq F] (entry : TreeLexEntry F α) (target : NanoTree F) : Decidable (entry.Matches target)

Equations

• Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq entry target = Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq._aux_1 entry target

The shared exponence core

@[instance_reducible]

instance Morphology.Nanosyntax.instRuleTreeLexEntryNanoTree {F : Type u_1} {α : Type u_2} : Exponence.Rule (TreeLexEntry F α) (NanoTree F) α

A tree lexical entry exposes the shared exponence core interface (Morphology.Exponence.Rule): contexts are syntactic targets, applicability is Superset-Principle matching.

Equations

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

@[instance_reducible]

instance Morphology.Nanosyntax.instPreorderTreeLexEntry {F : Type u_1} {α : Type u_2} : Preorder (TreeLexEntry F α)

Equations

• Morphology.Nanosyntax.instPreorderTreeLexEntry = Morphology.Exponence.toPreorder

theorem Morphology.Nanosyntax.TreeLexEntry.le_iff {F : Type u_1} {α : Type u_2} {a b : TreeLexEntry F α} : a ≤ b ↔ b.tree.Contains a.tree

The specificity order is reverse containment of the stored trees: a is at least as specific as b exactly when b's tree contains a's. Tree size is therefore a faithful specificity measure (Contains.size_le), which is what licenses smallest-tree selection.

Tree spellout (Elsewhere Condition)

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableRelTreeLexEntryNanoTreeApplies {F : Type u_1} {α : Type u_2} [DecidableEq F] : DecidableRel Exponence.Applies

Equations

• Morphology.Nanosyntax.instDecidableRelTreeLexEntryNanoTreeApplies e t = Morphology.Nanosyntax.instDecidableMatchesOfDecidableEq e t

def Morphology.Nanosyntax.treeSelect {F : Type u_1} {α : Type u_2} [DecidableEq F] (entries : List (TreeLexEntry F α)) (target : NanoTree F) : Option (TreeLexEntry F α)

The matching entry with the smallest stored tree (first-listed on ties): Minimize Junk over tree-generalized Superset matching, as the shared core's Exponence.selectBy at the tree-size score dualized so the smallest tree wins.

Equations

• Morphology.Nanosyntax.treeSelect entries target = Morphology.Exponence.selectBy (fun (e : Morphology.Nanosyntax.TreeLexEntry F α) => OrderDual.toDual e.tree.size) entries target

def Morphology.Nanosyntax.treeSpellout {F : Type u_1} {α : Type u_2} [DecidableEq F] (entries : List (TreeLexEntry F α)) (target : NanoTree F) : Option α

Phrasal spellout via the tree-generalized Superset Principle: among entries whose tree contains the target, select the one with the smallest tree (most specific match).

Parallels Morphology.Containment.spellout, but the matching relation is tree containment instead of rank comparison, and the specificity metric is tree size instead of rank.

Equations

• Morphology.Nanosyntax.treeSpellout entries target = Option.map (fun (x : Morphology.Nanosyntax.TreeLexEntry F α) => x.exponent) (Morphology.Nanosyntax.treeSelect entries target)

theorem Morphology.Nanosyntax.treeSelect_isElsewhereWinner {F : Type u_1} {α : Type u_2} [DecidableEq F] {entries : List (TreeLexEntry F α)} {target : NanoTree F} {e : TreeLexEntry F α} (h : treeSelect entries target = some e) : Exponence.IsElsewhereWinner entries target e

Smallest-tree selection is an Elsewhere winner of the shared core: the dualized-size score is strictly antitone in specificity (size_strictAnti), so a size-minimal match is maximally specific. An instance of selectBy_isElsewhereWinner.

theorem Morphology.Nanosyntax.treeSpellout_isElsewhereWinner {F : Type u_1} {α : Type u_2} [DecidableEq F] {entries : List (TreeLexEntry F α)} {target : NanoTree F} {x : α} (h : treeSpellout entries target = some x) : ∃ e ∈ entries, e.exponent = x ∧ Exponence.IsElsewhereWinner entries target e

The spelled-out exponent is an Elsewhere winner's exponent.

Foot Condition

def Morphology.Nanosyntax.FootConditionMet {F : Type u_1} {α : Type u_2} (entry : TreeLexEntry F α) (syntacticTree : NanoTree F) : Prop

The Foot Condition ([TTML18]): the foot of a lexical entry's stored tree must be present as a feature in the syntactic structure being spelled out.

If entry M stores [X [...[Z]]], the Foot Condition requires that Z appear in the structure. This constrains backtracking: when spellout fails and the derivation splits the target into specifier + complement, only entries whose foot matches a feature in the remaining structure are eligible.

Equations

• Morphology.Nanosyntax.FootConditionMet entry syntacticTree = syntacticTree.Contains (Morphology.Nanosyntax.NanoTree.leaf entry.tree.foot)

@[instance_reducible]

instance Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq {F : Type u_1} {α : Type u_2} [DecidableEq F] (entry : TreeLexEntry F α) (tree : NanoTree F) : Decidable (FootConditionMet entry tree)

Equations

• Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq entry tree = Morphology.Nanosyntax.instDecidableFootConditionMetOfDecidableEq._aux_1 entry tree

Chain trees (bridge to 1D)

def Morphology.Nanosyntax.chainTree {F : Type u_1} (feat : ℕ → F) : ℕ → NanoTree F

Build a right-branching chain tree of depth n. chainTree feat 0 = leaf (feat 0) chainTree feat 1 = node (feat 1) [leaf (feat 0)] chainTree feat n = node (feat n) [chainTree feat (n-1)]

A chain of depth n is isomorphic to an SpanRule spanning grade n in the 1D nanosyntax.

Equations

• Morphology.Nanosyntax.chainTree feat 0 = Morphology.Nanosyntax.NanoTree.leaf (feat 0)
• Morphology.Nanosyntax.chainTree feat n.succ = Morphology.Nanosyntax.NanoTree.node (feat (n + 1)) [Morphology.Nanosyntax.chainTree feat n]

Bridge theorems

theorem Morphology.Nanosyntax.chainTree_succ {F : Type u_1} (feat : ℕ → F) (n : ℕ) : chainTree feat (n + 1) = NanoTree.node (feat (n + 1)) [chainTree feat n]

theorem Morphology.Nanosyntax.chainTree_size {F : Type u_1} (feat : ℕ → F) (n : ℕ) : (chainTree feat n).size = n + 1

Chain tree size is n + 1 (one node per feature level).

theorem Morphology.Nanosyntax.chainTree_foot {F : Type u_1} (feat : ℕ → F) (n : ℕ) : (chainTree feat n).foot = feat 0

The foot of a chain tree is always feat 0 — the bottom of the functional sequence.

theorem Morphology.Nanosyntax.chainTree_injective {F : Type u_1} (feat : ℕ → F) : Function.Injective (chainTree feat)

Chains of distinct depths are distinct trees, regardless of the feature assignment — depth alone separates them.

theorem Morphology.Nanosyntax.chain_contains_iff_le {F : Type u_1} (feat : ℕ → F) (re r : ℕ) : (chainTree feat re).Contains (chainTree feat r) ↔ r ≤ re

For right-branching chains, tree containment reduces to rank comparison: a chain of depth re contains a chain of depth r iff r ≤ re. This is exactly the matching condition of the rank-based SpanRule.Matches, establishing that tree-based spellout generalizes (not replaces) rank-based spellout.

Unlike the previous Bool formulation, no injectivity of feat is needed: chain depth alone drives both directions.

Rose-tree interface instances

NanoTree joins the Core.Order.Branching tower. The structural size/decEq/decContains above remain the kernel-computable specializations ([file-level generality discipline]: WF-derived generics do not kernel-reduce, so decide-style spell-out evaluations need the structural forms).

@[instance_reducible]

instance Morphology.Nanosyntax.NanoTree.instBranching {F : Type u_1} : Core.Order.Branching (NanoTree F)

Equations

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

@[simp]

theorem Morphology.Nanosyntax.NanoTree.branching_children_leaf {F : Type u_1} (f : F) : Core.Order.Branching.children (leaf f) = []

@[simp]

theorem Morphology.Nanosyntax.NanoTree.branching_children_node {F : Type u_1} (f : F) (cs : List (NanoTree F)) : Core.Order.Branching.children (node f cs) = cs

instance Morphology.Nanosyntax.NanoTree.instIsFiniteBranching {F : Type u_1} : Core.Order.IsFiniteBranching (NanoTree F)