Construction DSL and accessors for syntactic objects

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

Construction discipline

The Merge operator (SyntacticObject.node/SyntacticObject.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: SyntacticObject.ofPlanar (SyntacticObject.nodeP (SyntacticObject.leafP tok₁) (SyntacticObject.leafP tok₂)). SyntacticObject.node_mk (skeleton) relates such a build to SyntacticObject.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 — SyntacticObject.isTrace is just · = SyntacticObject.traceLeaf.

Computable planar construction DSL

@[reducible, inline]

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

Planar builder: a lexical leaf.

Equations

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

@[reducible, inline]

abbrev Minimalist.SyntacticObject.traceP : RoseTree SOLabel

Planar builder: the bare trace leaf.

Equations

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

@[reducible, inline]

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

Planar builder: a bare binary node.

Equations

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

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

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.SyntacticObject.ofPlanar p h = ⟨RoseTree.Nonplanar.mk p, h⟩

@[simp]

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

@[simp]

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instInhabited : Inhabited SyntacticObject

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

Equations

• Minimalist.SyntacticObject.instInhabited = { default := Minimalist.SyntacticObject.traceLeaf }

Merge as multiplication

@[instance_reducible]

noncomputable instance Minimalist.SyntacticObject.instMul : Mul SyntacticObject

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

Equations

• Minimalist.SyntacticObject.instMul = { mul := Minimalist.SyntacticObject.node }

@[simp]

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

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

The canonical Merge operators (carrier primitives)

SyntacticObject.merge / SyntacticObject.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 (SyntacticObject.merge_toForest / SyntacticObject.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.SyntacticObject.merge (S S' : SyntacticObject) : SyntacticObject

External Merge on the carrier ([MCB25] Lemma 1.4.1): the bare binary node SyntacticObject.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.SyntacticObject.merge_val (S S' : SyntacticObject) : ↑(S.merge S') = RoseTree.Nonplanar.node (Sum.inr ()) {↑S, ↑S'}

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

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 SyntacticObject.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.SyntacticObject.intMerge_val (mover remainder : SyntacticObject) : ↑(mover.intMerge remainder) = RoseTree.Nonplanar.node (Sum.inr ()) {↑remainder, ↑mover}

Lexical-leaf construction (the legacy mkLeaf API)

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

A lexical leaf from a category and selectional stack.

Equations

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

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

A lexical leaf with a phonological form.

Equations

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

Accessors

def Minimalist.SyntacticObject.getLIToken (s : SyntacticObject) : 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.SyntacticObject.getLIToken_lexLeaf (tok : LIToken) : (lexLeaf tok).getLIToken = some tok

@[simp]

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

@[simp]

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

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem Minimalist.SyntacticObject.isTrace_traceLeaf : traceLeaf.isTrace

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

Leaf count (number of leaves + traces).

Equations

• s.leafCount = (↑s).numLeaves

def Minimalist.SyntacticObject.isLeaf (s : SyntacticObject) : 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.SyntacticObject.isNode (s : SyntacticObject) : Bool

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

Equations

• s.isNode = !s.isLeaf

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instRepr : Repr SyntacticObject

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

decide demonstrations