Derivation steps on the SO carrier

P4-pre-b of the single-carrier program: the ordered derivation layer on the SO carrier — the sequence of Merge/Move operations producing a syntactic object — replacing the legacy FreeCommMagma-based Step/Derivation.

The derivation's Merge is the workspace Merge by construction. Each step applies a canonical MCB Merge operator (Workspace.lean): External Merge is SO.merge (Lemma 1.4.1), Internal Merge is SO.intMerge (Prop 1.4.2's M_{T/β,β}) on the deletion remainder SO.deleteAccessible mover current (= T/mover). So Step.apply unfolds to the coproduct operators (SO.Step.apply_emL/apply_im); the Δ^ρ-coproduct identity is SO.merge_toForest/SO.intMerge_toForest — nothing is independently stipulated then bridged.

Index-free traces (D2): Internal Merge leaves the bare SO.traceLeaf; chain identity is workspace-level (Workspace, chainMultiplicity, #795, MCB Def 1.2.1), not a per-step Nat. The deletion remainder is realized by SO.replace (#804): for a uniquely-accessible mover this is exactly the Δ^ρ cut remainder SO.intMerge_toForest extracts, and replace-all is its total extension to the multi-occurrence (chain) case.

Because SO.node is noncomputable, so are Step.apply/Derivation.final — concrete trees are reasoned about structurally, not by decide. The computable, decide-able surface order (externalization replay + the Π bridge, the Cinque-style word-order readout) is the separate research-grade follow-up; it replays the linear choices on an ordered planar accumulator, since final (a Nonplanar quotient) is unordered.

Steps

inductive Minimalist.SO.Step : Type

A single derivation step on the SO carrier. Index-free (D2): im records only the mover; the trace it leaves is the bare SO.traceLeaf, and the mover ↔ trace chain lives at the workspace level (#795), not in a per-step index.

• emL (item : SO) : Step

  External Merge, new item as the left daughter.

• emR (item : SO) : Step

  External Merge, new item as the right daughter.

• im (mover : SO) : Step

  Internal Merge: raise mover, leaving the bare trace in its place.

noncomputable def Minimalist.SO.deleteAccessible (mover current : SO) : SO

Internal-Merge deletion remainder T/mover ([MCB25] Def 1.2.7, the ρ-form): the syntactic object left when the moved constituent's accessible occurrence is cut, with the bare SO.traceLeaf in its place. For a uniquely-accessible mover this is the Δ^ρ deletion remainder p0.2 that SO.intMerge_toForest extracts from cutSummandsN; SO.replace (replace-all) is its total extension to the multi-occurrence case (the chain is then read at the workspace level, Def 1.2.1).

Equations

• mover.deleteAccessible current = current.replace mover Minimalist.SO.traceLeaf

@[simp]

theorem Minimalist.SO.deleteAccessible_val (mover current : SO) : ↑(mover.deleteAccessible current) = replaceN ↑mover ↑traceLeaf ↑current

noncomputable def Minimalist.SO.Step.apply (step : Step) (current : SO) : SO

Apply a derivation step to the current tree. The derivation Merge is the workspace Merge by construction: External Merge is SO.merge (Lemma 1.4.1), Internal Merge is SO.intMerge (Prop 1.4.2's M_{T/β,β}) applied to the deletion remainder SO.deleteAccessible mover current (= T/mover). The coproduct identity of each is SO.merge_toForest/SO.intMerge_toForest. Since SO.merge is commutative (SO.mul_comm), emL/emR and the mover-left/remainder-left orders give the same SO (apply_emL_eq_emR); the left/right distinction matters only for the surface (PF) order, recovered downstream by the externalization replay.

Equations

• (Minimalist.SO.Step.emL item).apply current = item.merge current
• (Minimalist.SO.Step.emR item).apply current = current.merge item
• (Minimalist.SO.Step.im mover).apply current = mover.intMerge (mover.deleteAccessible current)

theorem Minimalist.SO.Step.apply_emL (item current : SO) : (emL item).apply current = item.merge current

External Merge unfolds to the canonical workspace EM SO.merge (Lemma 1.4.1).

theorem Minimalist.SO.Step.apply_emR (item current : SO) : (emR item).apply current = current.merge item

External Merge unfolds to the canonical workspace EM SO.merge (Lemma 1.4.1).

theorem Minimalist.SO.Step.apply_im (mover current : SO) : (im mover).apply current = mover.intMerge (mover.deleteAccessible current)

Internal Merge unfolds to the coproduct operator by construction. The im step is the canonical workspace IM SO.intMerge (MCB Prop 1.4.2) on the deletion remainder — definitionally, not via a bridge. Composing with SO.intMerge_toForest gives the Δ^ρ-coproduct identity on the workspace.

theorem Minimalist.SO.Step.apply_emL_eq_emR (item current : SO) : (emL item).apply current = (emR item).apply current

External Merge is side-indifferent on the unordered carrier: emL and emR build the same syntactic object (they diverge only at externalization).

Derivations

structure Minimalist.SO.Derivation : Type

An ordered derivation: an initial SO together with a sequence of steps.

• initial : SO

  The initial syntactic object (a lexical item, in canonical derivations).

• steps : List Step

  The ordered sequence of Merge/Move steps.

noncomputable def Minimalist.SO.Derivation.final (d : Derivation) : SO

The final tree produced by applying every step in order.

Equations

• d.final = List.foldl (fun (so : Minimalist.SO) (step : Minimalist.SO.Step) => step.apply so) d.initial d.steps

noncomputable def Minimalist.SO.Derivation.stageAt (d : Derivation) (n : ℕ) : SO

The intermediate tree after the first n steps.

Equations

• d.stageAt n = List.foldl (fun (so : Minimalist.SO) (step : Minimalist.SO.Step) => step.apply so) d.initial (List.take n d.steps)

def Minimalist.SO.Derivation.length (d : Derivation) : ℕ

The number of derivation steps.

Equations

• d.length = d.steps.length

def Minimalist.SO.Derivation.movedItems (d : Derivation) : List SO

The movers — the subtrees that underwent Internal Merge.

Equations

• d.movedItems = List.filterMap (fun (x : Minimalist.SO.Step) => match x with | Minimalist.SO.Step.im mover => some mover | x => none) d.steps

@[simp]

theorem Minimalist.SO.Derivation.stageAt_zero (d : Derivation) : d.stageAt 0 = d.initial

Stage 0 is the initial tree (no steps applied).

theorem Minimalist.SO.Derivation.stageAt_length (d : Derivation) : d.stageAt d.steps.length = d.final

The stage at full length is the final tree.

Worked example

The movers of a small derivation are read directly off the steps (a filterMap, so this is decide-able even though final is not): a derivation that internally merges two objects records exactly those two as moved.

Derivation-grounded externalization (computable PF order)

[MCB25] §1.12. final is an unordered Nonplanar quotient, so the surface left-to-right order is not recoverable from it. But a Derivation records the planarization choices: emL/im place material on the LEFT edge, emR on the right — exactly MCB's externalization section σ_L, here fixed by the derivation ("the language L") rather than a noncanonical Quot.out. The fold below replays the steps on an ordered RoseTree SOLabel accumulator, giving a fully computable PF: it never calls the noncomputable SO.node/SO.replace (it uses planar tree surgery + a Nonplanar.mk equality test), so surface orders decide. Index-free traces are sound here: traces are unpronounced, dropped by planarYield.

The formal Π-bridge faithfulness theorem (SO.Derivation.externalizeP?_faithful, below) proves Nonplanar.mk externalizeP? = final whenever the replay succeeds: the surface readouts are the word order of the actual derived object, not just a replay that happens to reproduce attested orders. The decide demos below exercise concrete derivations.

def Minimalist.SO.toPlanarLeaf? (s : SO) : Option (RoseTree SOLabel)

Planar form of a leaf/trace SO (the only items merged in canonical derivations); none for a complex SO (no recorded internal order).

Equations

• s.toPlanarLeaf? = match s.getLIToken with | some tok => some (Minimalist.SO.leafP tok) | none => if s = Minimalist.SO.traceLeaf then some Minimalist.SO.traceP else none

def Minimalist.planarYield : RoseTree SOLabel → List LIToken

Plain left-to-right token yield of an already-ordered planar tree; traces (Sum.inr ()) are unpronounced and contribute nothing.

Equations

• Minimalist.planarYield (RoseTree.node (Sum.inl tok) children) = [tok]
• Minimalist.planarYield (RoseTree.node (Sum.inr PUnit.unit) []) = []
• Minimalist.planarYield (RoseTree.node (Sum.inr PUnit.unit) [l, r]) = Minimalist.planarYield l ++ Minimalist.planarYield r
• Minimalist.planarYield (RoseTree.node (Sum.inr PUnit.unit) children) = []

def Minimalist.projEqP (target : SO) (s : RoseTree SOLabel) : Bool

"Projects to target": a planar subtree whose nonplanar projection is the SO target — the predicate the im replay uses to locate a mover. Computable (DecidableEq (Nonplanar …)), so it decides.

Equations

• Minimalist.projEqP target s = decide (RootedTree.Nonplanar.mk s = ↑target)

def Minimalist.planarFindP? (p : RoseTree SOLabel → Bool) : RoseTree SOLabel → Option (RoseTree SOLabel)

Leftmost (root-first) subtree satisfying p.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.planarFindP? p (RoseTree.node value []) = if p (RoseTree.node value []) = true then some (RoseTree.node value []) else none
• Minimalist.planarFindP? p (RoseTree.node value children) = if p (RoseTree.node value children) = true then some (RoseTree.node value children) else none

def Minimalist.planarReplaceWhereP (p : RoseTree SOLabel → Bool) (rep : RoseTree SOLabel) : RoseTree SOLabel → RoseTree SOLabel

Replace every subtree satisfying p by rep.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.planarReplaceWhereP p rep (RoseTree.node value []) = if p (RoseTree.node value []) = true then rep else RoseTree.node value []
• Minimalist.planarReplaceWhereP p rep (RoseTree.node value children) = if p (RoseTree.node value children) = true then rep else RoseTree.node value children

def Minimalist.moveLeftPlanarP (acc : RoseTree SOLabel) (mover : SO) : Option (RoseTree SOLabel)

Internal Merge on the ordered accumulator: raise the leftmost subtree projecting to mover to the LEFT edge, leaving the bare trace SO.traceP. none if absent.

Equations

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

def Minimalist.externStepP (acc? : Option (RoseTree SOLabel)) (step : SO.Step) : Option (RoseTree SOLabel)

One externalization step on the ordered accumulator (mirrors SO.Step.apply).

Equations

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

def Minimalist.SO.Derivation.externalizeP? (d : Derivation) : Option (RoseTree SOLabel)

The derivation's ordered planar representative (MCB σ_L for this derivation), or none if a merged item is complex / a mover is missing.

Equations

• d.externalizeP? = d.initial.toPlanarLeaf?.bind fun (init : RoseTree Minimalist.SOLabel) => List.foldl Minimalist.externStepP (some init) d.steps

def Minimalist.SO.Derivation.surfaceTokens (d : Derivation) : List LIToken

Surface (pronounced) tokens, left-to-right; traces dropped. Empty if externalization fails.

Equations

• d.surfaceTokens = (Option.map Minimalist.planarYield d.externalizeP?).getD []

def Minimalist.SO.Derivation.surfaceCats (d : Derivation) : List Cat

Surface category sequence — the readout used by word-order studies.

Equations

• d.surfaceCats = List.map (fun (x : Minimalist.LIToken) => x.item.outerCat) d.surfaceTokens

def Minimalist.SO.Derivation.surfacePhon (d : Derivation) : List String

Surface phonological string: pronounced forms left-to-right (empty forms dropped).

Equations

• d.surfacePhon = List.filterMap (fun (t : Minimalist.LIToken) => have p := t.phonForm; if p.isEmpty = true then none else some p) d.surfaceTokens

Π-bridge faithfulness: Nonplanar.mk externalizeP? = final

[MCB25] §1.12. The externalization replay (externStepP on an ordered RoseTree SOLabel accumulator) is faithful to the abstract derived object: each planar op's Nonplanar.mk equals the corresponding noncomputable SO op, so whenever the replay succeeds its nonplanar projection is exactly final. This upgrades surfaceCats/surfacePhon from "validated by decide demos" to "provably the word order of the actual derived SO" — the guarantee the word-order studies (Cinque2005, ColeHermon2008, Chomsky1995, …) rely on.

theorem Minimalist.SO.Derivation.externalizeP?_faithful (d : Derivation) {p : RoseTree SOLabel} (h : d.externalizeP? = some p) : RootedTree.Nonplanar.mk p = ↑d.final

Π-bridge faithfulness ([MCB25] §1.12): whenever the computable externalization replay externalizeP? succeeds, its nonplanar projection is exactly the abstract derived object final. So the surface readouts (surfaceTokens/surfaceCats/surfacePhon) are provably the word order of the actual derived syntactic object — the guarantee the word-order studies depend on. The replay is partial by design (EM of a complex item / a missing mover ⇒ none, making the claim vacuous there); on the canonical leaf/trace derivations the studies build, it succeeds.

Verification: the [Cin05] pied-piping contrast

Phrasal pied-piping preserves the moved constituent's internal order, so deriving Dem-N-A-Num (raise N around A, then pied-pipe [N A] around Num) is distinct from Dem-A-N-Num (pied-pipe [A N] around Num). Movers are built with the computable DSL so the surface orders decide. (.D stands in for the demonstrative.)