Externalization on the SO carrier (selection-induced order)

[MCB25] §1.12.1 / Lemma 1.13.5 / Lemma 1.13.7. P3c-1 of the single-carrier program: the externalization section on the SO carrier, recast as a selection-induced planar order. By Lemma 1.13.7 the externalization section σ_L is the selection structure, so the surface order is computable, section-free, and PermEquiv-liftable exactly like selCheck (P3a) — there is no Quot.out and the HeadFunction.section_ : FreeCommMagma.Section field disappears on SO.

At a bare binary node the projecting (selector) daughter (computed by selSide, Selection.lean) is placed on the language's convention side (ConventionDir: head- initial vs head-final, Lemma 1.13.5). Exocentric nodes — off Dom(h), where σ_L is explicitly noncanonical — are ordered by the canonical cmpList cmpTok comparison (RepOrder.lean), the list analogue of the legacy smallerFirst; this keeps the order fully computable and PermEquiv-invariant.

The §1.13 head function on SO is the selection head (SO.head := SO.selHead, already P3a); the head at an internal vertex v (a subterm) is v.head.

Out of scope (P3c-2 / P4): the structural phase domain (phaseComplement/ phaseInterior, via P2 subterms) and the flip SyntacticObject := SO.

Yield combinators

def Minimalist.placeYield : ConventionDir → List LIToken → List LIToken → List LIToken

Place the head daughter's yield on the convention side: .initial (head-initial) → head-yield first, .final (head-final) → head-yield last. The list-level analogue of placeHead (Selection.lean).

Equations

• Minimalist.placeYield Minimalist.ConventionDir.initial x✝¹ x✝ = x✝¹ ++ x✝
• Minimalist.placeYield Minimalist.ConventionDir.final x✝¹ x✝ = x✝ ++ x✝¹

def Minimalist.exoYield (a b : List LIToken) : List LIToken

Exocentric tie-break ([MCB25] Lemma 1.13.5, the noncanonical case off Dom(h)): order the two yields by the canonical cmpList cmpTok comparison (RepOrder.lean) — the list analogue of smallerFirst. Commutative (exoYield_comm), so it descends to the quotient.

Equations

• Minimalist.exoYield a b = if Minimalist.cmpList Minimalist.cmpTok a b = Ordering.gt then b ++ a else a ++ b

theorem Minimalist.exoYield_comm (a b : List LIToken) : exoYield a b = exoYield b a

exoYield is commutative: cmpList cmpTok is an antisymmetric strict-total comparison (cmpList_swap/cmpList_eq), so the choice is argument-order independent. Mirrors smallerFirst_comm.

Linearization on the planar carrier

def Minimalist.linearizeP (side : ConventionDir) : RoseTree SOLabel → List LIToken

Selection-induced externalization yield on a planar SO-tree ([MCB25] Lemma 1.13.5). A lexical leaf is pronounced ([tok]); a bare trace leaf is unpronounced ([]); a bare binary node places the projecting (selector) daughter on the side-convention side (placeYield), with the exocentric fallback exoYield. Section-free and computable (no Quot.out): the order is selection-determined, so it is PermEquiv-invariant.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.linearizeP side (RoseTree.node (Sum.inl tok) children) = [tok]
• Minimalist.linearizeP side (RoseTree.node (Sum.inr PUnit.unit) []) = []
• Minimalist.linearizeP side (RoseTree.node (Sum.inr PUnit.unit) children) = []

theorem Minimalist.linearizeP_permEquiv (side : ConventionDir) {t s : RoseTree SOLabel} (h : t.PermEquiv s) : linearizeP side t = linearizeP side s

linearizeP side is PermEquiv-invariant, so it descends to the quotient: the surface order is projection-determined, not representative-position-determined.

def Minimalist.linearizeN (side : ConventionDir) : RootedTree.Nonplanar SOLabel → List LIToken

Linearization lifted to the nonplanar carrier.

Equations

• Minimalist.linearizeN side = RootedTree.Nonplanar.lift (Minimalist.linearizeP side) ⋯

@[simp]

theorem Minimalist.linearizeN_mk (side : ConventionDir) (p : RoseTree SOLabel) : linearizeN side (RootedTree.Nonplanar.mk p) = linearizeP side p

theorem Minimalist.linearizeN_node (side : ConventionDir) (a b : RootedTree.Nonplanar SOLabel) : linearizeN side (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) = match selSide (selCheckN a) (selCheckN b) with | some true => placeYield side (linearizeN side a) (linearizeN side b) | some false => placeYield side (linearizeN side b) (linearizeN side a) | none => exoYield (linearizeN side a) (linearizeN side b)

Externalization on SO

def Minimalist.SO.linearize (side : ConventionDir) (s : SO) : List LIToken

Externalization ([MCB25] §1.12.1 / Lemma 1.13.5): the surface token order of a syntactic object under the head-side convention side. Selection-induced (the projecting daughter goes head-side), section-free, and computable — the SO-carrier replacement for the legacy HeadFunction.linearize (which composed linearizePlanar with a Quot.out section_).

Equations

• Minimalist.SO.linearize side s = Minimalist.linearizeN side ↑s

def Minimalist.SO.phonYield (side : ConventionDir) (s : SO) : List String

Phonological yield: the surface order, keeping only pronounced (non-empty phonForm) tokens. Traces, being the bare Sum.inr () leaf, contribute nothing.

Equations

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

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

The §1.13 / §1.15 head function on SO: the projecting (selector) head, by c-selection ([MCB25] Lemma 1.13.7 = [Adg03] "the item that projects is the item that selects"). This is the selection head (P3a) under the head-function name; the head at an internal vertex v (a subterm) is v.head.

Equations

• s.head = s.selHead

@[simp]

theorem Minimalist.SO.linearize_lexLeaf (side : ConventionDir) (tok : LIToken) : linearize side (lexLeaf tok) = [tok]

@[simp]

theorem Minimalist.SO.linearize_traceLeaf (side : ConventionDir) : linearize side traceLeaf = []

theorem Minimalist.SO.linearize_node (side : ConventionDir) (l r : SO) : linearize side (l.node r) = match selSide l.selCheck r.selCheck with | some true => placeYield side (linearize side l) (linearize side r) | some false => placeYield side (linearize side r) (linearize side l) | none => exoYield (linearize side l) (linearize side r)

@[simp]

theorem Minimalist.SO.head_lexLeaf (tok : LIToken) : (lexLeaf tok).head = some tok

theorem Minimalist.SO.head_node {l r : SO} {h : LIToken} (hlr : (l.node r).head = some h) : l.head = some h ∨ r.head = some h

Head Feature Principle on SO ([MCB25] Lemma 1.13.7 / [Adg03]): a node's head is one of its daughters' heads — so the §1.15 head function labels each internal vertex by (the head of) the projecting daughter. The carrier analogue of the legacy selHead_mul.

decide demonstration

The selection-induced order reduces on concrete mk-built trees and the head-side parameter genuinely flips the surface order. A determiner the (category D, selecting N) over a noun dog: D projects, so head-initial yields the dog and head-final yields dog the.