Selection-driven heads on the SyntacticObject carrier

This file defines the c-selection head of a syntactic object: whichever sister's head selects the saturated other projects — Adger 2003's identification of the projecting item with the selecting item, instantiating the bare-phrase-structure projection (Chomsky 1995 §4) that Marcolli et al. 2025 §1.13.3 abstracts as head functions (Definition 1.13.6 / Lemma 1.13.7). Like the book's head functions it is partial: 0 at exocentric nodes.

Main declarations

• Minimalist.SelectionState: a constituent's selection state — the projecting head with its residual selectional stack; a CommMagma and MulZeroClass, with 0 the off-Dom(h) failure.
• Mul SelectionState and Minimalist.selSide: the carrier-free combinators — the selection product, and which daughter projects.
• Minimalist.selNode, Minimalist.selCheckPlanar, Minimalist.SyntacticObject.selCheck: the selection algebra (SyntacticObject.mergeAlgebra), its catamorphism, and the carrier lift.
• Minimalist.SyntacticObject.selHead, Minimalist.SyntacticObject.cat?: the head token and its category, the head function of the phases (SyntacticObject.IsPhaseHead).
• Minimalist.SyntacticObject.selCheckHom: selCheck as a morphism of magmas SyntacticObject →ₙ* SelectionState, via SyntacticObject.lift.

Main results

• mul_comm (via CommMagma SelectionState) and Minimalist.selSide_comm: order-independence — the formal content of Merge's unordered output.
• Head SelectionState: the head of a selection product is a factor's head, so selHead is endocentric (Minimalist.mem_head_or_mem_head_of_mem_head_map_mul).
• Minimalist.SyntacticObject.selHead_map: a relabelling that preserves selection commutes with the selection-driven head.
• Minimalist.SelectionState.isSaturated_iff_not_isSaturated_of_mul_ne_zero, Minimalist.SelectionState.head_mul_of_not_isSaturated: Merge is triggered, one factor selecting and the other saturated, and the selecting factor projects.

Implementation notes

SelectionState is a one-field structure over Option (LexicalItem.Token × List Cat), so that the selection product can be an instance on it: the Option is implementation, and 0 is the public spelling of the exocentric failure, the off-domain value of a partial head function. There is no One, since two saturated states multiply to 0, and no associativity claim, so the structure is CommMagma + MulZeroClass only. The trace of a token is a lower copy of the phrase it heads, so it gets that phrase's value, saturated with the token's category (traceState), and a head that selected the moved phrase still selects its trace; the bare trace remembers no token and gets the saturated dummy .of .bareTrace []. selCheck reads only the token's category and sel. Two saturated sisters have no head, as in Marcolli et al. 2025's partial head functions: a specifier and its sister are labeled, if at all, by the labeling algorithm (Label/MinimalSearch.lean).

References

• Adger 2003, Core Syntax: A Minimalist Approach
• Chomsky 1995, Bare Phrase Structure
• Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized
• Collins & Stabler 2016, A Formalization of Minimalist Syntax