Agree (Minimalist Feature Checking)

Formalization of Agree following [Cho00] and [Adg03].

Agree is the mechanism by which features are checked/valued:

1. A probe (head with unvalued feature) searches its c-command domain
2. It finds the closest goal (element with matching valued feature)
3. The probe's feature is valued by copying from the goal
4. Both features are then checked (and may delete at PF/LF)

This file states Agree's structural conditions over SyntacticObject trees (c-command locality, horizons, phase-boundedness) and the valuation step over FeatureBundles. Bundles live in a feature assignment LIToken → FeatureBundle rather than in the carrier — the free-Merge core keeps SO₀ features atomic (Features/Slot.lean) — and a constituent exposes its projecting head's bundle through selection-driven labeling (headBundle). The feature types live in Features.lean; the search kernel and failure model ([Pre14] Ch. 5) in Probe/Basic.lean; richer satisfaction conditions ([Dea24], [Kei19]) in Probe/Satisfaction.lean; the Case Filter in Syntax/Case/Filter.lean.

Agree relations

Feature bundles live in a feature assignment LIToken → FeatureBundle, not in the carrier (Features/Slot.lean). A constituent exposes its projecting head's bundle through selection-driven labeling (SyntacticObject.selHead), so an Agree relation's feature conditions and its structural conditions are read off one tree and one assignment.

def Minimalist.headBundle (feats : LIToken → FeatureBundle) (s : SyntacticObject) : FeatureBundle

The feature bundle s exposes to Agree under the assignment feats: its projecting head's bundle. An unlabelable constituent exposes no features (⊥), so it can neither probe nor serve as a goal.

Equations

• Minimalist.headBundle feats s = (Option.map feats s.selHead).getD ⊥

@[simp]

theorem Minimalist.headBundle_lexLeaf (feats : LIToken → FeatureBundle) (tok : LIToken) : headBundle feats (SyntacticObject.lexLeaf tok) = feats tok

def Minimalist.validAgree (feats : LIToken → FeatureBundle) (root probe goal : SyntacticObject) (t : FeatureType) : Prop

Valid Agree under a feature assignment: probe c-commands goal in root, the probe's head bears an unvalued t-slot, and the goal's head bears a valued one.

Equations

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

@[instance_reducible]

instance Minimalist.instDecidableValidAgree (feats : LIToken → FeatureBundle) (root probe goal : SyntacticObject) (t : FeatureType) : Decidable (validAgree feats root probe goal t)

Equations

• Minimalist.instDecidableValidAgree feats root probe goal t = id inferInstance

theorem Minimalist.validAgree_irrefl (feats : LIToken → FeatureBundle) (root s : SyntacticObject) (t : FeatureType) : ¬validAgree feats root s s t

Nothing Agrees with itself: one slot cannot be both unvalued and valued. Irreflexivity is a fact about the assignment being a single source of feature truth, not about c-command (a multiply-occurring subterm can c-command itself).

Locality: closest goal

"Closest matching goal, no intervener" is canonically the list engine Probe.search (Probe/Basic.lean, search_eq_some_iff_closest, with pred playing Probe.vis). SyntacticObject is a commutative magma with no canonical c-command linearization, so the tree↔list bridge is not definitional; isClosestGoalIn is the decidable tree-native presentation.

def Minimalist.isClosestGoalIn (root probe goal : SyntacticObject) (pred : SyntacticObject → Bool) : Prop

goal is a closest pred-goal for probe in root: pred-matching and c-commanded by probe, with no pred-matching node c-commanded by probe c-commanding goal.

Equations

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

@[instance_reducible]

instance Minimalist.instDecidableIsClosestGoalIn (root probe goal : SyntacticObject) (pred : SyntacticObject → Bool) : Decidable (isClosestGoalIn root probe goal pred)

Equations

• Minimalist.instDecidableIsClosestGoalIn root probe goal pred = id (have this := Multiset.decidableExistsMultiset; inferInstance)

Horizons ([Kei19])

@[instance_reducible]

instance Minimalist.instDecidableIsHorizonLeafFor (horizonCat : Cat) (n : SyntacticObject) : Decidable (Minimalist.isHorizonLeafFor✝ horizonCat n)

Equations

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

def Minimalist.behindHorizonIn (root probe target : SyntacticObject) (horizonCat : Cat) : Prop

target is behind a horizon of category horizonCat for probe in root: some horizonCat leaf sits in probe's search domain and c-commands target, rendering it invisible ([Kei19]).

Example: N° is a horizon for wh-probes ([AP25]). In [DP D° [PossP Psr N°]], N° c-commands Psr, so wh-probes on C° cannot reach Psr; D° is not c-commanded by N°, so the whole DP stays visible for pied-piping.

The canonical list-native horizon specification is Probe.Profile (Probe/Profile.lean); this is the tree-native presentation.

Equations

• Minimalist.behindHorizonIn root probe target horizonCat = ∃ n ∈ root.subtrees, Minimalist.isHorizonLeafFor✝ horizonCat n ∧ root.cCommandsIn n target ∧ root.cCommandsIn probe n

@[instance_reducible]

instance Minimalist.instDecidableBehindHorizonIn (root probe target : SyntacticObject) (horizonCat : Cat) : Decidable (behindHorizonIn root probe target horizonCat)

Equations

• Minimalist.instDecidableBehindHorizonIn root probe target horizonCat = Multiset.decidableExistsMultiset

Feature valuation

def Minimalist.applyAgree (probeFeats goalFeats : FeatureBundle) (t : FeatureType) : Option FeatureBundle

Apply Agree: value the probe's feature from the goal. If the goal has a valued feature at dimension t and the probe's t-slot is unvalued, the probe's slot is set to that value; none when the goal has nothing to transmit.

Equations

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

Phase-bounded Agree

def Minimalist.validAgreeWithPIC (strength : PICStrength) (phases : List Phase) (feats : LIToken → FeatureBundle) (root probe goal : SyntacticObject) (t : FeatureType) : Prop

Agree bounded by the Phase Impenetrability Condition: valid Agree whose goal every phase admits extraction from (Phase.admitsExtraction). Under strong/weak this blocks goals frozen in a phase interior; under linearizationBound ([SCD26]) the phasehood layer is transparent and locality falls to Cyclic Linearization.

Equations

• Minimalist.validAgreeWithPIC strength phases feats root probe goal t = (Minimalist.validAgree feats root probe goal t ∧ ∀ ph ∈ phases, Minimalist.admitsExtraction strength ph goal)

@[instance_reducible]

instance Minimalist.instDecidableValidAgreeWithPIC (strength : PICStrength) (phases : List Phase) (feats : LIToken → FeatureBundle) (root probe goal : SyntacticObject) (t : FeatureType) : Decidable (validAgreeWithPIC strength phases feats root probe goal t)

Equations

• Minimalist.instDecidableValidAgreeWithPIC strength phases feats root probe goal t = id inferInstance

applyAgree as a Probe transmission

def Minimalist.phiProbe (t : FeatureType) : Probe FeatureBundle

The φ-probe: relativized search ([BR03]/[Pre14]) for a goal bearing a valued feature at dimension t.

Equations

• Minimalist.phiProbe t = Minimalist.Probe.ofVis fun (gf : Minimalist.FeatureBundle) => (gf.getValuedFeature t).isSome

theorem Minimalist.applyAgree_is_phi_transmit (probeFeats : FeatureBundle) (t : FeatureType) {goals : List FeatureBundle} {gf : FeatureBundle} (h : (phiProbe t).search goals = some gf) : (phiProbe t).transmit (fun (g pf : FeatureBundle) => (applyAgree pf g t).getD pf) probeFeats goals = (applyAgree probeFeats gf t).getD probeFeats

applyAgree is the φ goal→probe transmission. A φ-Agree is Probe.transmit of the φ-probe with the valuation applyAgree: search the goal sequence for a t-bearing goal, then value the probe's features from it. This recognizes the standalone applyAgree as the transmission step of the unified Agree operation (Probe/Transmission.lean), rather than a parallel mechanism. (The probe→goal direction — dependent case — and a full clause's worth of valuations are folds of transmits: the composition axis, not a single transmit.)