Derivation-grounded externalization (computable PF order)

[MCB25] §1.12. SyntacticObject.Derivation.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. externalizeP? replays the steps on an ordered RoseTree SOLabel accumulator, giving a fully computable PF: it never calls the noncomputable SyntacticObject.node/SyntacticObject.replace (planar tree surgery + a Nonplanar.mk equality test), so surface orders decide. Traces are unpronounced, dropped by planarYield.

The Π-bridge faithfulness theorem SyntacticObject.Derivation.externalizeP?_faithful proves Nonplanar.mk externalizeP? = final whenever the replay succeeds: the surface readouts (surfaceTokens/surfaceCats/surfacePhon) are the word order of the actual derived object. Sibling accounts of linearization: the selection-induced harmonic order (Linearization/Externalization.lean) and Fox-Pesetsky cyclic linearization (Linearization/Cyclic.lean).

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 SyntacticObject.node/SyntacticObject.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 (SyntacticObject.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.SyntacticObject.toPlanarLeaf? (s : SyntacticObject) : Option (RoseTree SOLabel)

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

Equations

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

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 : SyntacticObject) (s : RoseTree SOLabel) : Bool

"Projects to target": a planar subtree whose nonplanar projection is the SyntacticObject 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 : SyntacticObject) : Option (RoseTree SOLabel)

Internal Merge on the ordered accumulator: raise the leftmost subtree projecting to mover to the LEFT edge, leaving the bare trace SyntacticObject.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 : SyntacticObject.Step) : Option (RoseTree SOLabel)

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

Equations

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

def Minimalist.SyntacticObject.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.SyntacticObject.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.SyntacticObject.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.SyntacticObject.Derivation.surfacePhon (d : Derivation) : List String

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

Equations

• d.surfacePhon = List.filterMap Minimalist.LIToken.phonForm? 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 SyntacticObject 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 SyntacticObject" — the guarantee the word-order studies (Cinque2005, ColeHermon2008, Chomsky1995, …) rely on.

theorem Minimalist.SyntacticObject.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.)