C-Selection and Derivation Well-Formedness

@cite{adger-2003} @cite{marcolli-chomsky-berwick-2025}

Implements Adger's c-selectional checking system over linglib's Minimalism substrate. Theories/Syntax/Minimalism/Derivation.lean defines free Merge (Step.apply); this file adds the orthogonal layer of feature checking that filters which derivations satisfy Full Interpretation.

Adger's apparatus

• (104) Full Interpretation: the structure at the semantic interface contains no uninterpretable features
• (105) Checking Requirement: uninterpretable features must be checked, then they delete
• (106) Checking under Sisterhood: an uninterpretable feature [uF] on a syntactic object Y is checked when Y is sister to another syntactic object Z which bears a matching feature F
• (110) kiss [V, uN]: an interpretable [V] feature plus an uninterpretable c-selectional [uN] feature
• (132) Merge applies to two SOs forming a new SO; only at the root
• (133) Definition of Head: the head is the SO that selects in any Merge operation
• (137) Headedness: the item that projects is the item that selects

M-C-B alignment: head info lives in the derivation

Per @cite{marcolli-chomsky-berwick-2025} §1.13.3 / §1.15, NEW Minimalism keeps SyntacticObject label-free (= FreeMagma LIToken here) and treats head functions as external partial maps Dom(h) ⊂ SO → LIToken. linglib follows this discipline:

• For derivation-based code, the head is tracked through the derivation history in SelectionalState.head. Derivation.headLI? and Derivation.outerCat? are then total for leaf-initial derivations (no heuristic involved).
• For arbitrary FreeMagma LIToken values not coming from a derivation, the leftmost-leaf heuristic in Basic.lean's outerCat provides a partial extension. This is HeadFunction.leftSpine in HeadFunction.lean.

Step.emR item is first Merge (complement): the head's outermost selectional feature is checked against item.outerCat, and the complement itself must be saturated (no remaining unchecked features). The projecting head does not change. Step.emL item is second Merge (specifier): no consumption — in linglib's flat encoding, specifiers are added by an operation distinct from c-selection-driven first Merge (Adger's split between V and little v puts the subject in spec,vP via EPP rather than via V's c-selection). The projecting head does not change.

Key definitions

• SelectionalState — bundles a SyntacticObject with the projecting head's LIToken and its remaining unchecked selectional features
• SyntacticObject.checkedSel? — recursively checks a built tree for internal c-selection consistency, returning the head's residual pending stack (heuristic-based, used internally for complex emR items)
• Step.applyChecked — applies a step under c-selection, returning none when checking fails (eq. 134 Checking Requirement); preserves head info
• Derivation.checkedFinal? — runs the derivation through applyChecked, seeding head from the initial leaf
• Derivation.headLI? / Derivation.outerCat? — total head accessors for derivation-based code (M-C-B §1.13.3 head function via derivation tracking)
• Derivation.WellFormed — Adger's Full Interpretation: derivation completes with empty pending stack
• nullD / nullDWrap — Adger ch. 7 (DP): silent D head wrapping a bare N to project a DP that satisfies a verb's [uD] c-selection

Design notes

• Step.apply is unchanged. Free Merge and feature checking are separated, mirroring Adger's split between Merge as a structural operation (Ch 3 §3.2) and the Checking Requirement as a separate constraint (§3.5.3).
• Complex complements are checked recursively via checkedSel?, which enforces (a) internal saturation of the complement and (b) match between the head's pending feature and the complement's outerCat. This handles null-D-wrapped DPs (Adger ch. 7) where the complement is (∅, NP) with ∅'s [uN] checked internally before the whole DP is offered to the verb.
• Leftmost-leaf head heuristic survives only for the partial extension to arbitrary FreeMagmas (in outerCat and checkedSel?). For derivation-based head info, see Derivation.headLI? / outerCat? — these are total via M-C-B §1.13.3 derivation tracking.

structure Minimalist.SelectionalState : Type

A SyntacticObject paired with the projecting head's LIToken (per @cite{marcolli-chomsky-berwick-2025} §1.13.3) and its remaining uninterpretable c-selectional features.

Convention: features are consumed left-to-right by sister emR (complement Merge). The state is empty (pending = []) iff the head's selectional requirements have all been checked (Adger's Full Interpretation).

• so : SyntacticObject

  The current syntactic object.

• head : LIToken

  The projecting head's lexical item, tracked through the derivation (M-C-B §1.13.3 head function evaluated at the root vertex).

• pending : List Cat

  Remaining uninterpretable c-selectional features on the projecting head, in the order they will be checked.

@[implicit_reducible]

instance Minimalist.instReprSelectionalState : Repr SelectionalState

Equations

• Minimalist.instReprSelectionalState = { reprPrec := Minimalist.instReprSelectionalState.repr }

def Minimalist.instReprSelectionalState.repr : SelectionalState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqSelectionalState : DecidableEq SelectionalState

Equations

• Minimalist.instDecidableEqSelectionalState = Minimalist.instDecidableEqSelectionalState.decEq

def Minimalist.instDecidableEqSelectionalState.decEq (x✝ x✝¹ : SelectionalState) : Decidable (x✝ = x✝¹)

Equations

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

checkedSel? — parameterized over a head function

checkedSel? h so recursively checks an SO is built consistent with Adger 2003 c-selection (eq. 106 Checking under Sisterhood, eq. 132 Merge at root). Returns the head's residual pending features after all internal checking, or none if the structure is ill-built.

For a leaf, returns the leaf's outerSel untouched.

For a node (l, r) of h.section_.σ so, the convention is: l is the projecting head (under harmonic head-initial), the complement r must be saturated (its checkedSelPlanar = some []), l's first pending feature is consumed by matching against r's outer category, and the residual is l's remaining stack.

def Minimalist.checkedSelWithPlanar (h : HeadFunction) : FreeMagma (LIToken ⊕ ℕ) → Option (List Cat)

Underlying parameterized checkedSel? on a planar FreeMagma representative.

For a binary node (l, r), computes the right child's outer category by leftmostLeafPlanar r |>.item.outerCat (or rightmostLeafPlanar r under head-final), staying entirely in the planar world. This avoids the externalize ∘ mk ≠ id round-trip bug: re-applying h.section_.σ to FreeCommMagma.mk r would target a potentially DIFFERENT representative than the r we already have in hand.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.checkedSelWithPlanar h (FreeMagma.of (Sum.inl tok)) = some tok.item.outerSel
• Minimalist.checkedSelWithPlanar h (FreeMagma.of (Sum.inr val)) = some []

def Minimalist.checkedSelWith? (h : HeadFunction) (so : SyntacticObject) : Option (List Cat)

Parameterized checkedSel?: under head function h (with externalize section), recursively check c-selection consistency on the planar representative h.section_.σ so. Computable when h.section_.σ is.

Not given as a SyntacticObject.checkedSelWith? dot-notation method because SyntacticObject := Quot _ doesn't admit dot-method projection through the quotient. Call as checkedSelWith? h so.

Equations

• Minimalist.checkedSelWith? h so = Minimalist.checkedSelWithPlanar h (h.section_.σ so)

@[simp]

theorem Minimalist.checkedSelWith?_leaf (h : HeadFunction) (tok : LIToken) : checkedSelWith? h (SyntacticObject.leaf tok) = some tok.item.outerSel

For a leaf SO, checkedSelWith? returns the leaf's outer selection list (independent of head function). Routes through Section.σ_of.

@[simp]

theorem Minimalist.checkedSelWith?_trace (h : HeadFunction) (n : ℕ) : checkedSelWith? h (SyntacticObject.trace n) = some []

For a trace SO, checkedSelWith? returns some [].

noncomputable def Minimalist.Step.applyChecked : Step → SelectionalState → Option SelectionalState

Apply a Step under c-selection (@cite{adger-2003} eq. 134 Checking Requirement, eq. 106 Checking under Sisterhood). The projecting head is preserved across all step constructors — this matches M-C-B §1.15 (the labeling algorithm assigns the same head to a node and its head daughter) and Adger eq. 137 ("Headedness").

• emR item (complement Merge) requires (a) the head's pending to be non-empty and its head category to match item.outerCat, and (b) item to be saturated (item.checkedSel? = some []). The matched feature is consumed; head unchanged.
• emL item (specifier Merge) does not consume selectional features; head unchanged.
• im and wlm propagate without consumption; head unchanged.

Returns none when checking fails (no pending feature, category mismatch, or unsaturated complement).

Equations

• One or more equations did not get rendered due to their size.
• (Minimalist.Step.emR item).applyChecked { so := so, head := head, pending := [] } = none
• (Minimalist.Step.emL item).applyChecked { so := so, head := head, pending := sel } = some { so := item.node so, head := head, pending := sel }
• (Minimalist.Step.im mover traceId).applyChecked { so := so, head := head, pending := sel } = some { so := (Minimalist.Step.im mover traceId).apply so, head := head, pending := sel }

noncomputable def Minimalist.Derivation.checkedFinal? (d : Derivation) : Option SelectionalState

Run a derivation through applyChecked. Seeds the head from the initial leaf (M-C-B §1.13.3: leaves are always in Dom(h)); for node-initial derivations falls back to HeadFunction.leftSpine.head. Returns none if the initial is ill-built or any step violates c-selection.

Equations

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

def Minimalist.Derivation.WellFormed (d : Derivation) : Prop

A derivation is well-formed (Adger's Full Interpretation, @cite{adger-2003} eq. 104+161) iff it completes with no unchecked selectional features remaining on the projecting head.

Equations

• d.WellFormed = (Option.map (fun (x : Minimalist.SelectionalState) => x.pending) d.checkedFinal? = some [])

@[implicit_reducible]

noncomputable instance Minimalist.instDecidableWellFormed (d : Derivation) : Decidable d.WellFormed

Equations

• Minimalist.instDecidableWellFormed d = id inferInstance

M-C-B-aligned head accessors

For derivation-based code, head info is tracked through the derivation rather than recovered via heuristics. These accessors implement M-C-B §1.13.3's head function for the leaf-initial case (which covers all canonical Minimalist derivations).

noncomputable def Minimalist.Derivation.headLI? (d : Derivation) : Option LIToken

The projecting head's lexical item, computed by tracking through the derivation. Returns some tok for derivations whose initial seed is .leaf tok and whose step sequence is well-formed under applyChecked; none otherwise.

This is the M-C-B §1.13.3 head function specialized to derivation history — total for leaf-initial well-formed derivations, with no leftmost-leaf heuristic.

Equations

• d.headLI? = Option.map (fun (x : Minimalist.SelectionalState) => x.head) d.checkedFinal?

noncomputable def Minimalist.Derivation.outerCat? (d : Derivation) : Option Cat

The projecting head's outer categorial feature (Adger eq. 110 [F]), derived from the tracked head. Total for leaf-initial well-formed derivations.

Equations

• d.outerCat? = Option.map (fun (x : Minimalist.LIToken) => x.item.outerCat) d.headLI?

Adger ch. 7: silent D for bare nominal arguments

@cite{adger-2003} ch. 7 (Functional Categories II — the DP) treats every argumental nominal as a DP. Bare common nouns (mass nouns, generic plurals) are headed by a phonologically silent D that projects DP and consumes the noun's [N] feature.

nullD id builds a silent D leaf with selectional feature [N] (so that it checks against an N complement); nullDWrap n id is the canonical "null-D-wraps-a-bare-N" construction, returning (nullD, n) whose outerCat is .D and whose checkedSel? is some [] (saturated).

def Minimalist.nullD (id : ℕ) : SyntacticObject

A silent D head bearing the c-selectional feature [N], used by nullDWrap to project a DP from a bare common noun (Adger ch. 7). The id argument should be unique within the derivation.

Equations

• Minimalist.nullD id = Minimalist.mkLeafPhon Minimalist.Cat.D [Minimalist.Cat.N] "" id

def Minimalist.nullDWrap (n : SyntacticObject) (id : ℕ) : SyntacticObject

Wrap a bare N (or any N-projecting SO) under a silent D, yielding a saturated DP suitable for use as a verb's [uD] complement. @cite{adger-2003} ch. 7.

Equations

• Minimalist.nullDWrap n id = (Minimalist.nullD id).node n

Angelopoulos 2026: silent light noun for [n]-feature checking

@cite{angelopoulos-2026} §3.1 (following @cite{arsenijevic-2009}, @cite{moltmann-2019}) analyses Greek oti/pu as bearing an uninterpretable [n]-feature checked by a silent light noun in their specifier. The light noun is then licensed by incorporation (@cite{hale-keyser-1993}) into a higher lexical head (v_State or v_Event); incorporation into a functional head (T) is impossible.

nullN id builds a saturated silent little-n leaf, parallel to nullD. It carries no further selectional features — its role is to be Merged into Spec,CP, where it checks the C head's [n]-feature, and subsequently to head-move into a hosting v. Uses the existing Cat.n constructor (Marantz 2001 / Distributed Morphology nominal categorizer); no new Cat constructor required.

def Minimalist.nullN (id : ℕ) : SyntacticObject

A silent light noun (n head) with no selectional features, used for checking a complementizer's [n]-feature in its specifier per @cite{angelopoulos-2026} §3.1. The id argument should be unique within the derivation. Mirrors nullD.

Equations

• Minimalist.nullN id = Minimalist.mkLeafPhon Minimalist.Cat.n [] "" id

@[simp]

theorem Minimalist.nullN_outerCat_leftSpine (id : ℕ) : HeadFunction.leftSpine.outerCat (nullN id) = Cat.n

@[simp]

theorem Minimalist.nullN_checkedSel_leftSpine (id : ℕ) : checkedSelWith? HeadFunction.leftSpine (nullN id) = some []

Step-level lemmas

Destructor lemmas describing how applyChecked interacts with each Step constructor. Front-loaded so consumers (paper-replication study files) can reason about specific derivations without unfolding foldl.

@[simp]

theorem Minimalist.applyChecked_emR_match (so item : SyntacticObject) (head : LIToken) (c : Cat) (rest : List Cat) (hsat : checkedSelWith? HeadFunction.leftSpine item = some []) (hcat : HeadFunction.leftSpine.outerCat item = c) : (Step.emR item).applyChecked { so := so, head := head, pending := c :: rest } = some { so := so.node item, head := head, pending := rest }

emR with a saturated, category-matching item consumes the first selectional feature; head is preserved. Stated against HeadFunction.leftSpine (the default head function used by Step.applyChecked).

theorem Minimalist.applyChecked_emR_empty (so item : SyntacticObject) (head : LIToken) : (Step.emR item).applyChecked { so := so, head := head, pending := [] } = none

emR on an empty pending stack fails (no feature to check).

theorem Minimalist.applyChecked_emL (so item : SyntacticObject) (head : LIToken) (sel : List Cat) : (Step.emL item).applyChecked { so := so, head := head, pending := sel } = some { so := item.node so, head := head, pending := sel }

emL (specifier Merge) preserves both pending stack and head.

theorem Minimalist.wellFormed_initial_no_sel (tok : LIToken) (h : tok.item.outerSel = []) : { initial := SyntacticObject.leaf tok, steps := [] }.WellFormed

A leaf-initial derivation with empty outerSel and no steps is well-formed (Adger eq. 104: vacuously satisfies Full Interpretation).

theorem Minimalist.checkedSel_nullDWrap_leaf (n : SyntacticObject) (id : ℕ) (_hN : HeadFunction.leftSpine.outerCat n = Cat.N) (_hsat : checkedSelWith? HeadFunction.leftSpine n = some []) : checkedSelWith? HeadFunction.leftSpine (nullDWrap n id) = some []

nullDWrap of any leaf whose outerCat = .N is saturated.

TODO Phase 3.B+: requires an externalize-respect hypothesis on the .node (nullD id) n merge to rewrite checkedSelWith? leftSpine past the binary node. The substantive fact (nullD wraps a saturated N to yield a saturated DP) is correct; the proof is queued.