Construction DSL and accessors for syntactic objects

[MCB25] §1.1. The computable construction layer and the read-back accessors for the SO carrier, completing P2's API parity with the legacy FreeCommMagma (LIToken ⊕ Nat) surface. Imports only the carrier skeleton.

Construction discipline

The Merge operator (SO.node/SO.merge) is noncomputable (the smart Nonplanar.node round-trips through Quotient.out). So concrete syntactic objects — the ones studies decide over — are built planar-first and quotiented once: SO.ofPlanar (SO.nodeP (SO.leafP tok₁) (SO.leafP tok₂)). SO.node_mk (skeleton) relates such a build to SO.node, so theorems stated over node/* still apply.

Index-free traces

A trace is a bare Sum.inr () leaf with no index (MCB Def 1.2.1: chain identity is workspace-level), so there is exactly one trace leaf — SO.isTrace is just · = SO.traceLeaf.

Computable planar construction DSL

@[reducible, inline]

abbrev Minimalist.SO.leafP (tok : LIToken) : RoseTree SOLabel

Planar builder: a lexical leaf.

Equations

• Minimalist.SO.leafP tok = RoseTree.node (Sum.inl tok) []

@[reducible, inline]

abbrev Minimalist.SO.traceP : RoseTree SOLabel

Planar builder: the bare trace leaf.

Equations

• Minimalist.SO.traceP = RoseTree.node (Sum.inr ()) []

@[reducible, inline]

abbrev Minimalist.SO.nodeP (l r : RoseTree SOLabel) : RoseTree SOLabel

Planar builder: a bare binary node.

Equations

• Minimalist.SO.nodeP l r = RoseTree.node (Sum.inr ()) [l, r]

def Minimalist.SO.ofPlanar (p : RoseTree SOLabel) (h : isSOPlanar p = true := by first | rfl | decide) : SO

Build a syntactic object from a planar tree, discharging well-formedness by decide (concrete trees) — the computable entry point for decide-based studies.

Equations

• Minimalist.SO.ofPlanar p h = ⟨RootedTree.Nonplanar.mk p, h⟩

@[simp]

theorem Minimalist.SO.ofPlanar_leafP (tok : LIToken) : ofPlanar (leafP tok) ⋯ = lexLeaf tok

@[simp]

theorem Minimalist.SO.ofPlanar_traceP : ofPlanar traceP ⋯ = traceLeaf

@[implicit_reducible]

instance Minimalist.instInhabitedSO : Inhabited SO

Default syntactic object: the bare trace leaf. Lets structures with an SO field be Inhabited/deriving Repr-free of bespoke witnesses.

Equations

• Minimalist.instInhabitedSO = { default := Minimalist.SO.traceLeaf }

Merge as multiplication

@[implicit_reducible]

noncomputable instance Minimalist.instMulSO : Mul SO

* is (External) Merge: the bare binary node. Noncomputable — build concrete trees with the planar DSL above, not *.

Equations

• Minimalist.instMulSO = { mul := Minimalist.SO.node }

@[simp]

theorem Minimalist.SO.mul_def (l r : SO) : l * r = l.node r

theorem Minimalist.SO.mul_comm (l r : SO) : l * r = r * l

The canonical Merge operators (carrier primitives)

SO.merge / SO.intMerge are the carrier-level Merge operators ([MCB25] Lemma 1.4.1 / Prop 1.4.2): they need only the bare binary node, so they live here. Their coproduct identity on the workspace Hopf algebra (SO.merge_toForest / SO.intMerge_toForest) lives in Workspace.lean, which imports the Merge algebra; this file stays algebra-free so decide-based consumers (e.g. the externalization replay in SyntacticObject/Derivation.lean) keep the computable DecidableEq (Nonplanar …) (#792) in scope.

noncomputable def Minimalist.SO.merge (S S' : SO) : SO

External Merge on the carrier ([MCB25] Lemma 1.4.1): the bare binary node SO.node is External Merge (for distinct workspace items) and the re-merge stage of Internal Merge. Noncomputable; build concrete results with the planar DSL + decide.

Equations

• S.merge S' = S.node S'

@[simp]

theorem Minimalist.SO.merge_val (S S' : SO) : ↑(S.merge S') = RootedTree.Nonplanar.node (Sum.inr ()) {↑S, ↑S'}

noncomputable def Minimalist.SO.intMerge (mover remainder : SO) : SO

Internal Merge on the carrier ([MCB25] Prop 1.4.2): re-Merge the mover with the deletion remainder remainder = T/mover (the M_{T/β, β} order: remainder left, mover right). IM is not a new structural primitive — it is SO.merge of the remainder and the mover. The mover ↔ trace correspondence (the chain) is read at the workspace level (Workspace.chainMultiplicity), not from an index.

Equations

• mover.intMerge remainder = remainder.merge mover

@[simp]

theorem Minimalist.SO.intMerge_val (mover remainder : SO) : ↑(mover.intMerge remainder) = RootedTree.Nonplanar.node (Sum.inr ()) {↑remainder, ↑mover}

Lexical-leaf construction (the legacy mkLeaf API)

def Minimalist.SO.mkLeaf (cat : Cat) (sel : SelStack) (id : ℕ) : SO

A lexical leaf from a category and selectional stack.

Equations

• Minimalist.SO.mkLeaf cat sel id = Minimalist.SO.lexLeaf { item := Minimalist.LexicalItem.simple cat sel, id := id }

def Minimalist.SO.mkLeafPhon (cat : Cat) (sel : SelStack) (phon : String) (id : ℕ) : SO

A lexical leaf with a phonological form.

Equations

• Minimalist.SO.mkLeafPhon cat sel phon id = Minimalist.SO.lexLeaf { item := Minimalist.LexicalItem.simple cat sel phon, id := id }

Accessors

def Minimalist.SO.getLIToken (s : SO) : Option LIToken

The lexical token at the root, if the root is a lexical leaf.

Equations

• s.getLIToken = match (↑s).rootValue with | Sum.inl tok => some tok | Sum.inr PUnit.unit => none

@[simp]

theorem Minimalist.SO.getLIToken_lexLeaf (tok : LIToken) : (lexLeaf tok).getLIToken = some tok

@[simp]

theorem Minimalist.SO.getLIToken_traceLeaf : traceLeaf.getLIToken = none

@[simp]

theorem Minimalist.SO.getLIToken_node (l r : SO) : (l.node r).getLIToken = none

def Minimalist.SO.isTrace (s : SO) : Prop

A trace is the unique bare trace leaf (chain identity is workspace-level).

Equations

• s.isTrace = (s = Minimalist.SO.traceLeaf)

@[implicit_reducible]

instance Minimalist.instDecidableIsTrace (s : SO) : Decidable s.isTrace

Equations

• Minimalist.instDecidableIsTrace s = Minimalist.instDecidableIsTrace._aux_1 s

@[simp]

theorem Minimalist.SO.isTrace_traceLeaf : traceLeaf.isTrace

def Minimalist.SO.leafCount (s : SO) : ℕ

Leaf count (number of leaves + traces).

Equations

• s.leafCount = (↑s).numLeaves

def Minimalist.SO.isLeaf (s : SO) : Bool

Is s a leaf (lexical or trace)? A leaf has a single vertex; a bare binary node has ≥ 2 leaves.

Equations

• s.isLeaf = (s.leafCount == 1)

def Minimalist.SO.isNode (s : SO) : Bool

Is s a (bare binary) internal node? The complement of SO.isLeaf.

Equations

• s.isNode = !s.isLeaf

@[simp]

theorem Minimalist.SO.isLeaf_lexLeaf (tok : LIToken) : (lexLeaf tok).isLeaf = true

@[simp]

theorem Minimalist.SO.isLeaf_traceLeaf : traceLeaf.isLeaf = true

@[simp]

theorem Minimalist.SO.isNode_lexLeaf (tok : LIToken) : (lexLeaf tok).isNode = false

@[implicit_reducible]

instance Minimalist.instReprSO : Repr SO

A lightweight Repr so structures with an SO field can deriving Repr. The full tree is a Nonplanar quotient (no faithful structural readout without Quot.out); for debugging surface order use SO.linearize.

Equations

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

def Minimalist.SO.nodeCount (s : SO) : ℕ

Internal-node count = leaf count − 1 (full binary tree).

Equations

• s.nodeCount = (↑s).numLeaves - 1

@[simp]

theorem Minimalist.SO.leafCount_lexLeaf (tok : LIToken) : (lexLeaf tok).leafCount = 1

@[simp]

theorem Minimalist.SO.leafCount_traceLeaf : traceLeaf.leafCount = 1

decide demonstrations