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 SyntacticObject 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 SyntacticObject 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') + the SyntacticObject naming flip (P2, landed), 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 SyntacticObject 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 Perm-invariant (so it lifts)

theorem Minimalist.isSOPlanar_perm {t s : RoseTree SOLabel} : t.Perm s → isSOPlanar t = isSOPlanar s

isSOPlanar is invariant under Perm, hence descends to the quotient. At a node the arity check is fixed by the equal children lengths and the recursive check by the PermList companion.

theorem Minimalist.isSOPlanarList_permList {cs ds : List (RoseTree SOLabel)} : RoseTree.PermList cs ds → isSOPlanarList cs = isSOPlanarList ds

isSOPlanarList is a conjunction over children, hence PermList-invariant.

The carrier: IsSO on Nonplanar + the SyntacticObject subtype

def Minimalist.isSO : RoseTree.Nonplanar SOLabel → Bool

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

Equations

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

@[simp]

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

def Minimalist.IsSO (t : RoseTree.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)

@[instance_reducible]

instance Minimalist.instDecidablePredNonplanarSOLabelIsSO : DecidablePred IsSO

Equations

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

def Minimalist.SyntacticObject : Type

The MCB-faithful syntactic object carrier: well-formed nonplanar trees over SOLabel. Formerly SO; renamed once the operations (P2) and the head function / Phase API (P3) were ported onto it.

Equations

• Minimalist.SyntacticObject = { t : RoseTree.Nonplanar Minimalist.SOLabel // Minimalist.IsSO t }

@[instance_reducible]

instance Minimalist.instDecidableEqSyntacticObject : DecidableEq SyntacticObject

Equations

• Minimalist.instDecidableEqSyntacticObject = 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). SyntacticObject.node is the structural binary constructor; Workspace.lean's SyntacticObject.merge/SyntacticObject.intMerge are its Merge semantics.

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

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

Equations

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

def Minimalist.SyntacticObject.traceLeaf : SyntacticObject

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

Equations

• Minimalist.SyntacticObject.traceLeaf = ⟨RoseTree.Nonplanar.leaf (Sum.inr ()), Minimalist.SyntacticObject.traceLeaf._proof_1⟩

theorem Minimalist.isSO_node_pair (a b : RoseTree.Nonplanar SOLabel) : isSO (RoseTree.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.SyntacticObject.node (l r : SyntacticObject) : SyntacticObject

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 = ⟨RoseTree.Nonplanar.node (Sum.inr ()) {↑l, ↑r}, ⋯⟩

@[simp]

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

theorem Minimalist.SyntacticObject.node_mk (pl pr : RoseTree SOLabel) (hl : IsSO (RoseTree.Nonplanar.mk pl)) (hr : IsSO (RoseTree.Nonplanar.mk pr)) : ↑(node ⟨RoseTree.Nonplanar.mk pl, hl⟩ ⟨RoseTree.Nonplanar.mk pr, hr⟩) = RoseTree.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.SyntacticObject.ind {motive : SyntacticObject → Prop} (lex : ∀ (tok : LIToken), motive (lexLeaf tok)) (trace : motive traceLeaf) (node : ∀ (l r : SyntacticObject), motive l → motive r → motive (l.node r)) (s : SyntacticObject) : motive s

Induction on syntactic objects ([MCB25] §1.1.3.1). Every SyntacticObject 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 SyntacticObject.node. Proved by strong induction on the node count (numNodes; the two daughters of a binary node are strictly smaller).

theorem Minimalist.SyntacticObject.exists_form (s : SyntacticObject) : (∃ (tok : LIToken), s = lexLeaf tok) ∨ s = traceLeaf ∨ ∃ (l : SyntacticObject) (r : SyntacticObject), 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.