The MCB-faithful syntactic-object carrier (skeleton)

[MCB25] §1.1. The single-carrier program (scratch/mcb-single-carrier-spec.md) moves syntactic objects onto the same Nonplanar carrier the Merge algebra already uses, exactly as the book intends ("syntactic objects… are the generators of the Hopf algebra", §1.2). This file is P0's carrier skeleton: the well-formed subset of Nonplanar (LIToken ⊕ Unit).

Faithful labelling (§1.1.3.1: "no labels at any non-leaf vertices")

MCB's SO is a binary, nonplanar rooted tree with leaves labelled by SO₀ (lexical items + features) and internal vertices bare — the head is not on the tree; it comes from a separate labelling algorithm (§1.15, the head function). So on Nonplanar (LIToken ⊕ Unit) (the algebra's α ⊕ β, β = Unit), role by arity:

• a lexical leaf carries Sum.inl tok — a lexical item (LIToken ≈ SO₀);
• a trace leaf carries Sum.inr () — bare (chain identity is workspace-level, MCB Def 1.2.1, not a per-leaf index; this replaces the legacy ⊕ Nat);
• an internal node carries Sum.inr () — bare, no head label (§1.15 supplies it).

Sum.inr () is the single structural/bare marker; trace-leaf vs. internal is childless vs. binary. IsSO pins this. This is the deliberate departure from the legacy toNonplanar image, which decorated internal nodes with the head (Sum.inl headLeaf) — that decoration is the head function applied, not the object.

Scope

The carrier + IsSO + decidability + the SO subtype, with the faithful three-role alphabet (lexical/trace leaves + bare internals). Out of scope (later phases): workspaces + Merge on the carrier (EM + IM-via-coproduct, MCB Prop 1.4.2 — uses the existing comul{D,C}N; P1 continued), the structural ops (contains/subtrees = Acc') + flip SyntacticObject := SO (P2), the head function + Phase API re-home (P3), retiring FreeCommMagma/toNonplanar (P4). See scratch/p1-spec-and-audit.md.

@[reducible, inline]

abbrev Minimalist.SOLabel : Type

The SO label alphabet, in the algebra's α ⊕ β form (α = LIToken lexical, β = Unit bare). Each role is fixed by arity, not by a third label:

• Sum.inl tok on a leaf — a lexical item (LIToken ≈ SO₀);
• Sum.inr () on a leaf — a trace (bare; chain identity is workspace-level, MCB Def 1.2.1, not a per-leaf index — this replaces the legacy ⊕ Nat);
• Sum.inr () on an internal node — bare (no head; §1.15 supplies it).

Sum.inr () is the single "structural/bare" marker; a trace and an internal vertex are the childless vs. binary occurrences of it. This is exactly the Nonplanar (α ⊕ β) (β = Unit) alphabet the existing τ-parameterised trace coproducts (comul{D,C}N) already speak.

Equations

• Minimalist.SOLabel = (Minimalist.LIToken ⊕ Unit)

Well-formedness IsSO (binary, lexical/trace leaves, bare internals)

def Minimalist.isSOPlanar : RoseTree SOLabel → Bool

Structural well-formedness of a planar syntactic object: a lexical node must be a leaf; a bare (inr ()) node is either a trace leaf (childless) or a binary internal node with well-formed children. Permutation-friendly so it lifts to the nonplanar quotient.

Equations

• Minimalist.isSOPlanar (RoseTree.node (Sum.inl val) cs) = cs.isEmpty
• Minimalist.isSOPlanar (RoseTree.node (Sum.inr PUnit.unit) cs) = ((cs.length == 0 || cs.length == 2) && Minimalist.isSOPlanarList cs)

def Minimalist.isSOPlanarList : List (RoseTree SOLabel) → Bool

Auxiliary: all children well-formed.

Equations

• Minimalist.isSOPlanarList [] = true
• Minimalist.isSOPlanarList (c :: cs) = (Minimalist.isSOPlanar c && Minimalist.isSOPlanarList cs)

isSOPlanar is PermEquiv-invariant (so it lifts)

theorem Minimalist.isSOPlanar_permEquiv {t s : RoseTree SOLabel} (h : t.PermEquiv s) : isSOPlanar t = isSOPlanar s

isSOPlanar is invariant under PermEquiv, hence descends to the quotient.

The carrier: IsSO on Nonplanar + the SO subtype

def Minimalist.isSO : RootedTree.Nonplanar SOLabel → Bool

Well-formed-SO check on the nonplanar carrier, lifted from isSOPlanar.

Equations

• Minimalist.isSO = RootedTree.Nonplanar.lift Minimalist.isSOPlanar ⋯

@[simp]

theorem Minimalist.isSO_mk (t : RoseTree SOLabel) : isSO (RootedTree.Nonplanar.mk t) = isSOPlanar t

def Minimalist.IsSO (t : RootedTree.Nonplanar SOLabel) : Prop

A tree on the carrier is a syntactic object ([MCB25] §1.1): binary, nonplanar; leaves are lexical (Sum.inl tok) or traces (Sum.inr ()), internal vertices bare (Sum.inr ()). Decidable (and decide-able, via Core/…/DecEq).

Equations

• Minimalist.IsSO t = (Minimalist.isSO t = true)

@[implicit_reducible]

instance Minimalist.instDecidablePredNonplanarSOLabelIsSO : DecidablePred IsSO

Equations

• Minimalist.instDecidablePredNonplanarSOLabelIsSO t = Minimalist.instDecidablePredNonplanarSOLabelIsSO._aux_1 t

def Minimalist.SO : Type

The MCB-faithful syntactic object carrier: well-formed nonplanar trees over SOLabel. This is the target type that will become SyntacticObject once the operations (P2) and the head function / Phase API (P3) are ported onto it.

Equations

• Minimalist.SO = { t : RootedTree.Nonplanar Minimalist.SOLabel // Minimalist.IsSO t }

@[implicit_reducible]

instance Minimalist.instDecidableEqSO : DecidableEq SO

Equations

• Minimalist.instDecidableEqSO = Subtype.instDecidableEq

Smart constructors: leaves and the bare binary node

The three faithful shapes (§1.1.3.1): a lexical leaf (Sum.inl tok), a trace leaf (bare Sum.inr (), index-free — chain identity is workspace-level, MCB Def 1.2.1), and a bare binary node (Sum.inr (), internal). SO.node is the structural binary constructor; Workspace.lean's SO.merge/SO.intMerge are its Merge semantics.

def Minimalist.SO.lexLeaf (tok : LIToken) : SO

A lexical leaf: a childless Sum.inl tok (an SO₀ item).

Equations

• Minimalist.SO.lexLeaf tok = ⟨RootedTree.Nonplanar.leaf (Sum.inl tok), ⋯⟩

def Minimalist.SO.traceLeaf : SO

The trace leaf: a childless, bare Sum.inr () vertex ([MCB25] Def 1.2.7's ρ-vertex), index-free.

Equations

• Minimalist.SO.traceLeaf = ⟨RootedTree.Nonplanar.leaf (Sum.inr ()), Minimalist.SO.traceLeaf._proof_1⟩

theorem Minimalist.isSO_node_pair (a b : RootedTree.Nonplanar SOLabel) : isSO (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) = (isSO a && isSO b)

isSO of a bare binary node is the conjunction of isSO on the two children: Sum.inr () at arity 2 is well-formed exactly when both daughters are. Quotient.inductionOn₂ reduces the smart node to a tree .node via node_mk_tree_list, then unfolds isSOPlanar's binary arm.

noncomputable def Minimalist.SO.node (l r : SO) : SO

The bare binary node ([MCB25] §1.1.3.1): the well-formed internal vertex over two syntactic objects, with no head label. Noncomputable (it uses the smart Nonplanar.node); build concrete results via node_mk + decide.

Equations

• l.node r = ⟨RootedTree.Nonplanar.node (Sum.inr ()) {↑l, ↑r}, ⋯⟩

@[simp]

theorem Minimalist.SO.node_val (l r : SO) : ↑(l.node r) = RootedTree.Nonplanar.node (Sum.inr ()) {↑l, ↑r}

theorem Minimalist.SO.node_mk (pl pr : RoseTree SOLabel) (hl : IsSO (RootedTree.Nonplanar.mk pl)) (hr : IsSO (RootedTree.Nonplanar.mk pr)) : ↑(node ⟨RootedTree.Nonplanar.mk pl, hl⟩ ⟨RootedTree.Nonplanar.mk pr, hr⟩) = RootedTree.Nonplanar.mk (RoseTree.node (Sum.inr ()) [pl, pr])

Construction bridge: a node of two mk-built objects is the single RoseTree binary node mk (.node (inr ()) [pl, pr]) — built without the smart node's Quotient.out, so concrete results are decide-able.

Induction and case analysis

theorem Minimalist.isSOPlanar_of_mem {cs : List (RoseTree SOLabel)} (h : isSOPlanarList cs = true) (c : RoseTree SOLabel) : c ∈ cs → isSOPlanar c = true

Every member of an isSOPlanarList-true list is itself isSOPlanar: the children of a well-formed node are well-formed.

theorem Minimalist.SO.ind {motive : SO → Prop} (lex : ∀ (tok : LIToken), motive (lexLeaf tok)) (trace : motive traceLeaf) (node : ∀ (l r : SO), motive l → motive r → motive (l.node r)) (s : SO) : motive s

Induction on syntactic objects ([MCB25] §1.1.3.1). Every SO is a lexical leaf, the (bare) trace leaf, or a bare binary node of two syntactic objects — the faithful analogue of the legacy SyntacticObject.ind (leaf/trace/mul), with the mul case the bare SO.node. Proved by strong induction on the node count (numNodes; the two daughters of a binary node are strictly smaller).

theorem Minimalist.SO.exists_form (s : SO) : (∃ (tok : LIToken), s = lexLeaf tok) ∨ s = traceLeaf ∨ ∃ (l : SO) (r : SO), s = l.node r

Case analysis ([MCB25] §1.1.3.1): every syntactic object is a lexical leaf, the bare trace leaf, or a bare binary node.

The SyntacticObject carrier

SyntacticObject is the linguistic-facing name for the MCB-faithful SO carrier ([MCB25] §1.1.3.1: binary, nonplanar, rooted trees with bare internal vertices). It is a reducible abbreviation, so dot-notation on a value s : SyntacticObject dispatches to the SO.* API for free. The former FreeCommMagma (LIToken ⊕ Nat) carrier (with head-decorated nodes and ⊕ Nat trace indices) has been retired in favour of this one.

@[reducible, inline]

abbrev Minimalist.SyntacticObject : Type

Equations

• Minimalist.SyntacticObject = Minimalist.SO