LF branch of Spell-Out

noncomputable def Minimalist.SyntacticObject.toLFTree (so : SyntacticObject) : Core.Tree.Tree Unit String

Convert a narrow-syntax SyntacticObject to an LF tree for compositional interpretation.

• Leaf tokens → Tree.leaf phonForm (terminal nodes keyed by phonological form, which interp uses for lexical lookup)
• Traces (id ≥ 10000) → Tree.tr n (indexed trace nodes, which interp evaluates as g(n) under assignment g)
• Binary nodes → Tree.bin left right (preserving structure)

Tree is planar (.bin a b ≠ .bin b a in general); this transfer therefore depends on a planar representative of the underlying FreeCommMagma. Phase 1.0 placeholder via Quot.out; Phase 2 will replace with LCA-derived linearization parameterized by head directionality.

Equations

• so.toLFTree = Minimalist.toLFTreePlanar✝ (Quot.out so)

@[reducible, inline]

noncomputable abbrev Minimalist.SyntacticObject.toPF : SyntacticObject → List LIToken

The PF branch of Spell-Out is HeadFunction.linearize parameterized over a head function: h.linearize : SyntacticObject → List LIToken. This alias pins to HeadFunction.leftSpine (= Quot.out-based representative under harmonic head-initial), matching the legacy linearize semantics.

Equations

• Minimalist.SyntacticObject.toPF = Minimalist.HeadFunction.leftSpine.linearize

Structural preservation — Phase 2 TODO

The previous structural preservation theorems (toLFTree_leaf, toLFTree_trace, toLFTree_node, toLFTree_merge and the YModelDemo end-to-end test) were written when SyntacticObject was a planar inductive (TraceTree) — they relied on rfl against the planar constructor pattern. After the nonplanar migration (Phase 1.0), Tree remains planar (.bin a b ≠ .bin b a) while SyntacticObject is nonplanar; toLFTree therefore goes through Quot.out (a noncomputable representative choice). The preservation theorems are not provable by rfl against an arbitrary representative.

Phase 2 plan. Replace Quot.out-based toLFTree with an LCA-derived linearization parameterized by head directionality, then restate preservation as "for the canonical planar representative (per the LCA), the structural correspondence holds". The YModelDemo end-to-end test will then be re-proved against that canonical form.

Keeping toLFTree itself as a noncomputable placeholder until that work lands. The constructor on the LF side (.leaf/.tr/.bin) is unchanged; the change is purely on the order preserved.