Minimalist Labeling (@cite{marcolli-chomsky-berwick-2025} §1.15)

The MCB §1.15 Labeling Algorithm: assign categorial labels to non-leaf vertices of a SyntacticObject via an externally-supplied HeadFunction. There is no canonical "the" label of an SO — labeling is parametric over the head function chosen by the analyst.

This file is the single source of truth for Minimalist labeling. The pre-MCB selection-driven algorithm (getCategory, label, labelCat, selects, sameLabel, projectsIn, isMaximalIn, isHeadIn, isPhraseIn, etc.) was deleted at 0.230.798 — it predated both linglib's MCB substrate and the @cite{marcolli-chomsky-berwick-2025} formalisation, and bridged-via-HeadFunction.selectionBased preservation was rejected as perpetuating the legacy mindset (selection determines projection) that MCB explicitly relaxes.

Public API

• labelVertex h T v — MCB Definition 1.15.2: the categorial label at vertex v of T under head function h. Returns none for leaves (which carry their LIToken's outerCat directly) and when T ∉ Dom(h).
• labelRoot h T = labelVertex h T T — root-label special case.
• isLabelable h T v — Prop: labelVertex h T v is some _.
• sameLabelAt h T x y — x and y carry the same label in T under h.
• isHeadOf h T x — x is a leaf token equal to h.head T (so x is the projecting head of T).
• projectsAt h T x — x ⊆ T, x is non-leaf, and labelVertex h T x = labelRoot h T (so x carries the same label as the root).

Choice of head function

For consumers without natural derivational context, the standard choices are HeadFunction.leftSpine (left-headed; canonical for English-like analyses) or HeadFunction.rightSpine (right-headed). For Studies with a Derivation, the per-paper head function lives on the derivation (see Selection.lean's Derivation.headLI?).

The MCB framework treats these as equally valid; the choice is per- analysis, not a property of the language faculty.

noncomputable def Minimalist.Labeling.labelVertex (h : HeadFunction) (T v : SyntacticObject) : Option Cat

The categorial label at vertex v of T under head function h, when T ∈ Dom(h). Returns none for leaf vertices (which carry their own LIToken's category directly, not a "label" in the head-function sense) and when T ∉ Dom(h).

Implements @cite{marcolli-chomsky-berwick-2025} §1.15 Labeling Algorithm in its default case: the projecting head's outer category. UNVERIFIED: the precise case structure (1-4 vs (i)-(iv) vs Chomsky 2013-style cases) needs to be checked against MCB Definition 1.15.2 in the published book; the docstring previously described "case 1" without page-level verification. The shared-feature fallback (corresponding to Chomsky 2013's {XP, YP} sharing-of-φ) is not yet implemented; deferred to next session along with the case-numbering verification.

Equations

• Minimalist.Labeling.labelVertex h T v = if h.Dom T then if v.isNode then some (h.head v).item.outerCat else none else none

noncomputable def Minimalist.Labeling.labelRoot (h : HeadFunction) (T : SyntacticObject) : Option Cat

The label at the root of T (a frequent special case).

Equations

• Minimalist.Labeling.labelRoot h T = Minimalist.Labeling.labelVertex h T T

@[simp]

theorem Minimalist.Labeling.labelRoot_node_in_dom (h : HeadFunction) (a b : SyntacticObject) (hT : h.Dom (a.node b)) : labelRoot h (a.node b) = some (h.head (a.node b)).item.outerCat

For T ∈ Dom(h) with T = .node a b, the root label is the outer category of h(T).

@[simp]

theorem Minimalist.Labeling.labelVertex_leaf (h : HeadFunction) (T : SyntacticObject) (tok : LIToken) : labelVertex h T (SyntacticObject.leaf tok) = none

Leaves never get a "label" from the algorithm — they carry their own LIToken's category.

theorem Minimalist.Labeling.labelVertex_not_in_dom (h : HeadFunction) (T v : SyntacticObject) (hT : ¬h.Dom T) : labelVertex h T v = none

When T ∉ Dom(h), the algorithm's default case fails (returns none); the shared-feature fallback (case 4) is not yet implemented.

def Minimalist.Labeling.isLabelable (h : HeadFunction) (T v : SyntacticObject) : Prop

A vertex is labelable by the algorithm iff labelVertex returns some _. Non-labelable vertices correspond to objects filtered out by the Externalization quotient map Π_L per @cite{marcolli-chomsky-berwick-2025} §1.15.

Equations

• Minimalist.Labeling.isLabelable h T v = ((Minimalist.Labeling.labelVertex h T v).isSome = true)

@[implicit_reducible]

noncomputable instance Minimalist.Labeling.instDecidableIsLabelable (h : HeadFunction) (T v : SyntacticObject) : Decidable (isLabelable h T v)

Equations

• Minimalist.Labeling.instDecidableIsLabelable h T v = id inferInstance

theorem Minimalist.Labeling.internal_vertex_labelable_in_dom (h : HeadFunction) (T a b : SyntacticObject) (hT : h.Dom T) : isLabelable h T (a.node b)

For T ∈ Dom(h), every internal vertex is labelable (default case applies).

def Minimalist.Labeling.sameLabelAt (h : HeadFunction) (T x y : SyntacticObject) : Prop

Two vertices x, y of T carry the same label under h.

Equations

• Minimalist.Labeling.sameLabelAt h T x y = (Minimalist.Labeling.labelVertex h T x = Minimalist.Labeling.labelVertex h T y ∧ (Minimalist.Labeling.labelVertex h T x).isSome = true)

@[implicit_reducible]

noncomputable instance Minimalist.Labeling.instDecidableSameLabelAt (h : HeadFunction) (T x y : SyntacticObject) : Decidable (sameLabelAt h T x y)

Equations

• Minimalist.Labeling.instDecidableSameLabelAt h T x y = id inferInstance

def Minimalist.Labeling.isHeadOf (h : HeadFunction) (T x : SyntacticObject) : Prop

x is the projecting head of T under h: x is a leaf whose token equals h.head T. Decidable on LIToken.DecidableEq.

Equations

• Minimalist.Labeling.isHeadOf h T x = match x.getLIToken with | some tok => h.head T = tok | none => False

@[implicit_reducible]

noncomputable instance Minimalist.Labeling.instDecidableIsHeadOf (h : HeadFunction) (T x : SyntacticObject) : Decidable (isHeadOf h T x)

Equations

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

def Minimalist.Labeling.projectsAt (h : HeadFunction) (T x : SyntacticObject) : Prop

x projects at vertex x of T under h: x is a non-leaf contained in T whose label equals T's root label. This is the MCB analogue of "x is on the projection path of the root head".

Equations

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

@[implicit_reducible]

noncomputable instance Minimalist.Labeling.instDecidableProjectsAt (h : HeadFunction) (T x : SyntacticObject) : Decidable (projectsAt h T x)

Equations

• Minimalist.Labeling.instDecidableProjectsAt h T x = id inferInstance

def Minimalist.Labeling.isMaximalAt (h : HeadFunction) (T x : SyntacticObject) : Prop

x is +max(imal) in T under h: x ⊆ T and no strict ancestor of x in T carries the same label. A linglib-formulated "maximal projection" predicate; not yet proved equivalent to @cite{marcolli-chomsky-berwick-2025} Lemma 1.14.1's terminus of a γ_ℓ projection path (which would require the §1.14 algebraic substrate).

Bounded over T.subtrees so the predicate is decidable. The implication form z ≠ x → ¬ sameLabelAt (rather than the disjunction ¬ sameLabelAt ∨ z = x) reads as "for every strict ancestor, labels disagree" — the standard mathlib idiom.

Equations

• Minimalist.Labeling.isMaximalAt h T x = (Minimalist.containsOrEq T x ∧ ∀ z ∈ T.subtrees, Minimalist.contains z x → z ≠ x → ¬Minimalist.Labeling.sameLabelAt h T x z)

@[implicit_reducible]

noncomputable instance Minimalist.Labeling.instDecidableIsMaximalAt (h : HeadFunction) (T x : SyntacticObject) : Decidable (isMaximalAt h T x)

Equations

• Minimalist.Labeling.instDecidableIsMaximalAt h T x = id inferInstance

theorem Minimalist.Labeling.isMaximalAt_iff_unbounded (h : HeadFunction) (T x : SyntacticObject) : isMaximalAt h T x ↔ containsOrEq T x ∧ ∀ (z : SyntacticObject), isTermOf z T → contains z x → z ≠ x → ¬sameLabelAt h T x z

isMaximalAt's bounded ∀ z ∈ T.subtrees quantifier is equivalent to the textbook unbounded ∀ z, isTermOf z T → ... form. The bounded form is taken as the canonical definition for decidability; this lemma anchors the soundness against the unbounded statement.

Restored from the pre-rewrite isMaximalIn_iff_bounded audit trail.

def Minimalist.Labeling.isMinimalAt (T x : SyntacticObject) : Prop

x is +min(imal) in T under h: x is a leaf in T. (MCB treats heads as leaves; +min adds the membership requirement.)

Equations

• Minimalist.Labeling.isMinimalAt T x = (Minimalist.isTermOf x T ∧ x.isLeaf)

@[implicit_reducible]

instance Minimalist.Labeling.instDecidableIsMinimalAt (T x : SyntacticObject) : Decidable (isMinimalAt T x)

Equations

• Minimalist.Labeling.instDecidableIsMinimalAt T x = id inferInstance

def Minimalist.Labeling.isHeadIn (h : HeadFunction) (T x : SyntacticObject) : Prop

A head in T: +min and −max (it projects). MCB §1.15 classification carried over.

Equations

• Minimalist.Labeling.isHeadIn h T x = (Minimalist.Labeling.isMinimalAt T x ∧ ¬Minimalist.Labeling.isMaximalAt h T x)

@[implicit_reducible]

noncomputable instance Minimalist.Labeling.instDecidableIsHeadIn (h : HeadFunction) (T x : SyntacticObject) : Decidable (isHeadIn h T x)

Equations

• Minimalist.Labeling.instDecidableIsHeadIn h T x = id inferInstance

@[reducible, inline]

abbrev Minimalist.Labeling.isPhraseIn (h : HeadFunction) (T x : SyntacticObject) : Prop

A phrase in T: +max. MCB §1.15 classification carried over. abbrev of isMaximalAt so the two names unify in elaboration — the legacy file separated them but the semantic content is identical.

Equations

• Minimalist.Labeling.isPhraseIn h T x = Minimalist.Labeling.isMaximalAt h T x