The selection-driven head on the SO carrier

[MCB25] §1.13 (Lemma 1.13.7). P3a of the single-carrier program: the selection-driven head function on the SO carrier — the section-free, computable head ([Adg03] "the item that projects is the item that selects"). Re-homes selCheck/selHead/outerCatC onto SO, the foundation the Phase API consumes (isPhaseHeadOf, P3b).

The carrier-free selection combinators selStep/selSide (commutative — selStep_comm/selSide_comm) live here: they operate purely on selection states (Option (LIToken × List Cat)), so they are shared by the SO-carrier tree recursion below and the legacy section-based Selection.lean. Only the tree recursion is re-homed onto RoseTree SOLabel + the SO lift, exactly as subtreesN (P2a-ii). Index-free traces (P1): a bare trace leaf gets the canonical saturated value (mkTraceToken 0, []) — selCheck reads only the token's category (.N) and outerSel ([]), both index-independent, so this is behaviour-equivalent to the legacy (mkTraceToken n, []).

Carrier-free selection combinators

selStep/selSide combine two sisters' selection-check results into the node's projecting head (selStep) and which daughter projects (selSide). Both are order-independent (selStep_comm/selSide_comm) — the formal content of Merge's unordered output — so they descend through the nonplanar quotient.

def Minimalist.selStep : Option (LIToken × List Cat) → Option (LIToken × List Cat) → Option (LIToken × List Cat)

Combine two sisters' selection-check results. Order-independent (symmetric, selStep_comm): whichever sister's head c-selects the saturated other projects, yielding its residual stack; none at exocentric nodes (neither or both qualify).

Equations

• Minimalist.selStep (some (ha, c :: rest)) (some (hb, [])) = if hb.item.outerCat = c then some (ha, rest) else none
• Minimalist.selStep (some (ha, [])) (some (hb, c :: rest)) = if ha.item.outerCat = c then some (hb, rest) else none
• Minimalist.selStep x✝¹ x✝ = none

theorem Minimalist.selStep_comm (x y : Option (LIToken × List Cat)) : selStep x y = selStep y x

theorem Minimalist.selStep_fst {x y : Option (LIToken × List Cat)} {r : LIToken} (h : Option.map (fun (x : LIToken × List Cat) => x.1) (selStep x y) = some r) : Option.map (fun (x : LIToken × List Cat) => x.1) x = some r ∨ Option.map (fun (x : LIToken × List Cat) => x.1) y = some r

The head of selStep x y (when defined) is one of x/y's heads.

def Minimalist.selSide : Option (LIToken × List Cat) → Option (LIToken × List Cat) → Option Bool

Which daughter projects at a binary node under c-selection: some true = the left sister is the selector, some false = the right, none = exocentric (neither uniquely selects the saturated other). Mirrors selStep.

Equations

• Minimalist.selSide (some (ha, c :: rest)) (some (hb, [])) = if hb.item.outerCat = c then some true else none
• Minimalist.selSide (some (ha, [])) (some (hb, c :: rest)) = if ha.item.outerCat = c then some false else none
• Minimalist.selSide x✝¹ x✝ = none

theorem Minimalist.selSide_comm (x y : Option (LIToken × List Cat)) : selSide x y = Option.map not (selSide y x)

theorem Minimalist.selStep_eq_some {x y : Option (LIToken × List Cat)} {hd : LIToken} {res : List Cat} (h : selStep x y = some (hd, res)) : selSide x y = some true ∧ Option.map (fun (x : LIToken × List Cat) => x.1) x = some hd ∨ selSide x y = some false ∧ Option.map (fun (x : LIToken × List Cat) => x.1) y = some hd

When selStep returns a head, that head is the projecting daughter's head, and selSide agrees on which daughter projects. The bridge between the residual-tracking selStep and the order-determining selSide.

Selection check on the planar carrier

def Minimalist.selCheckPlanar : RoseTree SOLabel → Option (LIToken × List Cat)

Selection check on a planar SO-tree: the projecting head + residual pending features, or none outside the endocentric domain. Lexical leaf ↦ its token + outerSel; bare trace leaf ↦ canonical (mkTraceToken 0, []) (index-free); bare binary node ↦ selStep of the daughters.

Equations

• Minimalist.selCheckPlanar (RoseTree.node (Sum.inl tok) children) = some (tok, tok.item.outerSel)
• Minimalist.selCheckPlanar (RoseTree.node (Sum.inr PUnit.unit) []) = some (Minimalist.mkTraceToken 0, [])
• Minimalist.selCheckPlanar (RoseTree.node (Sum.inr PUnit.unit) [l, r]) = Minimalist.selStep (Minimalist.selCheckPlanar l) (Minimalist.selCheckPlanar r)
• Minimalist.selCheckPlanar (RoseTree.node (Sum.inr PUnit.unit) children) = none

theorem Minimalist.selCheckPlanar_permEquiv {t s : RoseTree SOLabel} (h : t.PermEquiv s) : selCheckPlanar t = selCheckPlanar s

selCheckPlanar is PermEquiv-invariant, so it descends to the quotient.

def Minimalist.selCheckN : RootedTree.Nonplanar SOLabel → Option (LIToken × List Cat)

Selection check lifted to the nonplanar carrier.

Equations

• Minimalist.selCheckN = RootedTree.Nonplanar.lift Minimalist.selCheckPlanar ⋯

@[simp]

theorem Minimalist.selCheckN_mk (p : RoseTree SOLabel) : selCheckN (RootedTree.Nonplanar.mk p) = selCheckPlanar p

theorem Minimalist.selCheckN_node (a b : RootedTree.Nonplanar SOLabel) : selCheckN (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) = selStep (selCheckN a) (selCheckN b)

The selection-driven head on SO

def Minimalist.SO.selCheck (s : SO) : Option (LIToken × List Cat)

Selection-driven head check on SO ([MCB25] Lemma 1.13.7): the projecting head + residual features, or none off the endocentric domain. Section-free and computable.

Equations

• s.selCheck = Minimalist.selCheckN ↑s

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

The projecting head's lexical item, by c-selection.

Equations

• s.selHead = Option.map (fun (x : Minimalist.LIToken × List Minimalist.Cat) => x.1) s.selCheck

def Minimalist.SO.checkedSel (s : SO) : Option (List Cat)

Residual pending selectional features (some [] = saturated).

Equations

• s.checkedSel = Option.map (fun (x : Minimalist.LIToken × List Minimalist.Cat) => x.2) s.selCheck

def Minimalist.SO.outerCatC (s : SO) : Option Cat

The projecting head's outer category (the phase-head selector, [MCB25] Lemma 1.13.7); none at exocentric nodes.

Equations

• s.outerCatC = Option.map (fun (x : Minimalist.LIToken) => x.item.outerCat) s.selHead

@[simp]

theorem Minimalist.SO.selCheck_lexLeaf (tok : LIToken) : (lexLeaf tok).selCheck = some (tok, tok.item.outerSel)

@[simp]

theorem Minimalist.SO.selCheck_traceLeaf : traceLeaf.selCheck = some (mkTraceToken 0, [])

@[simp]

theorem Minimalist.SO.selCheck_node (l r : SO) : (l.node r).selCheck = selStep l.selCheck r.selCheck

@[simp]

theorem Minimalist.SO.selHead_lexLeaf (tok : LIToken) : (lexLeaf tok).selHead = some tok

@[simp]

theorem Minimalist.SO.outerCatC_lexLeaf (tok : LIToken) : (lexLeaf tok).outerCatC = some tok.item.outerCat

decide demonstration