Nested Agree [Ama25]

A configuration on a Minimalist SyntacticObject: a single head bears two (or more) ordered probes that share a goal-head, and each post-initial probe's search domain is restricted to the daughters of the shared goal. The matryoshka structure is derived from cCommandsIn (the Minimalist substrate), not stipulated.

Configuration

A NestedAgreeConfig packages:

1. stack : OrderedProbeStack — ordered probes; head of list = first.
2. root : SyntacticObject — the tree under consideration.
3. probingHead : SyntacticObject — the head bearing the probes.
4. goalHead : SyntacticObject — the shared goal targeted under MME.
5. validGoal : SyntacticObject → Bool — lexical primitive: which subtrees carry active φ-features. Defective v of unaccusatives gets false; this is what blocks π-Agree in [Ama25]'s §3.4.2 unaccusative analysis.

initialDomain, daughters, searchDomain are derived via cCommandsIn and reflexive containment, filtered by validGoal. The matryoshka claim — post-initial domains restricted to the goal's daughters — is structural, not axiomatic. Consequently IsNestedAgreeConfig is non-vacuous: it requires goalHead to be both c-commanded by probingHead in root and phi-active.

Cross-domain applications

Italian aux selection (§3) is formalized at Studies/Amato2025.lean. Other Amato 2025 §4 case studies (Icelandic DAT-NOM, Lak perfective, Spanish VOS, Bulgarian wh, ditransitives) are deferred — their consumers will construct SyntacticObject trees and validGoal predicates the same way.

Architecture

Sits at Layer 2 (compositional Agree pattern), built on the Layer-1 substrate (SyntacticObject, cCommandsIn, containsOrEq, subtrees) imported transitively via Probe. Predicates are Prop with [Decidable] instances; runStack returns Option SyntacticObject.

Sibling mechanisms in Syntax/Minimalism/

Syntax/Minimalism/CyclicAgree.lean ([BR09]) and Long-Distance Agree ([Sza09], Studies/Allotey2021.lean) are sibling Layer-2 patterns. All three address "what does a probe do beyond its first operation," but the answers differ:

• Nested Agree (this file): multiple ordered probes on a single head, all forced to target the same goal under maximized matching; each subsequent probe operates on a truncated search domain restricted to the prior goal's daughters.
• Cyclic Agree (CyclicAgree.lean): a single articulated probe with multiple feature segments; cycle I targets the IA, cycle II targets the EA via the expanded residue domain. Subsequent cycles see more (residue + EA), not less.
• Long-Distance Agree (Studies/Allotey2021.lean): a single probe in the matrix relaxes locality across a non-defective C, reaching an embedded goal.

The three are conceptually orthogonal mechanisms for serial probing. A unified theory of probe behavior would treat them as alternatives in the design space; we keep them as independent Layer-2 patterns that consumers select by phenomenon.

@[reducible, inline]

abbrev Amato2025.NestedAgree.OrderedProbeStack : Type

An ordered list of probes on a single head. The list order encodes the feature-checking order: head of list = first probe.

Equations

• Amato2025.NestedAgree.OrderedProbeStack = List Minimalist.Probe.Profile

structure Amato2025.NestedAgree.NestedAgreeConfig : Type

A Nested Agree configuration on a Minimalist SyntacticObject.

• stack : OrderedProbeStack

  Ordered probes on the probing head.

• root : Minimalist.SyntacticObject

  The root tree under consideration.

• probingHead : Minimalist.SyntacticObject

  The head bearing the probes (e.g. Perf in Italian aux selection).

• goalHead : Minimalist.SyntacticObject

  The shared goal head every probe targets under maximized matching (e.g. v in Italian aux selection).

• validGoal : Minimalist.SyntacticObject → Bool

  Lexical primitive: which subtrees carry active φ-features. Defective v of unaccusatives gets false. Distinct from any derivational fact about whether Agree succeeded.

def Amato2025.NestedAgree.NestedAgreeConfig.length (c : NestedAgreeConfig) : ℕ

Number of probes in the stack.

Equations

• c.length = List.length c.stack

def Amato2025.NestedAgree.NestedAgreeConfig.initialDomain (c : NestedAgreeConfig) : Multiset Minimalist.SyntacticObject

Probe 0's c-command domain, filtered by phi-activity. Derived from cCommandsIn (Minimalist c-command on SyntacticObject).

subtrees returns Multiset (post-Phase-1.0; MCB-faithful per Def 1.2.2), so the filtered domain is also Multiset. Membership checks (goalHead ∈ initialDomain) work identically to the prior List flavor.

Equations

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

def Amato2025.NestedAgree.NestedAgreeConfig.daughters (c : NestedAgreeConfig) : Multiset Minimalist.SyntacticObject

The shared goal's daughters: the goal itself plus everything it c-commands, filtered by phi-activity. The reflexive inclusion of goalHead is required by maximized matching — every post-initial probe must be able to find the goal again.

Equations

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

def Amato2025.NestedAgree.NestedAgreeConfig.searchDomain (c : NestedAgreeConfig) : ℕ → Multiset Minimalist.SyntacticObject

Search domain at probe i: derived from the structural primitives. The matryoshka claim is encoded definitionally — searchDomain (i+1) = daughters for all i ≥ 0.

Equations

• c.searchDomain 0 = c.initialDomain
• c.searchDomain n.succ = c.daughters

def Amato2025.NestedAgree.IsNestedAgreeConfig (c : NestedAgreeConfig) : Prop

A bona fide Nested Agree configuration: the shared goal lies in probe 0's c-command domain and is phi-active. Non-vacuous: derives a structural claim about root (via cCommandsIn) plus the lexical primitive (validGoal). When phi-Agree fails (unaccusative v has validGoal = false), this predicate is correctly false — the formal expression of [Ama25]'s "the chain breaks down at π-Agree."

Equations

• Amato2025.NestedAgree.IsNestedAgreeConfig c = (c.goalHead ∈ c.initialDomain)

@[implicit_reducible]

instance Amato2025.NestedAgree.instDecidableIsNestedAgreeConfig (c : NestedAgreeConfig) : Decidable (IsNestedAgreeConfig c)

Equations

• Amato2025.NestedAgree.instDecidableIsNestedAgreeConfig c = id inferInstance

def Amato2025.NestedAgree.runStack (c : NestedAgreeConfig) (i : ℕ) : Option Minimalist.SyntacticObject

Run probe i against its derived search domain. Returns the shared goal when visible at index i, else none.

Equations

• Amato2025.NestedAgree.runStack c i = if i < c.length ∧ c.goalHead ∈ c.searchDomain i then some c.goalHead else none

theorem Amato2025.NestedAgree.runStack_some_iff (c : NestedAgreeConfig) (i : ℕ) : (runStack c i).isSome = true ↔ i < c.length ∧ c.goalHead ∈ c.searchDomain i

def Amato2025.NestedAgree.NestedAgreeConfig.goalProbe (c : NestedAgreeConfig) : Minimalist.Probe Minimalist.SyntacticObject

The goal-seeking probe: visible exactly at the shared goal. Nested Agree's locality lives in searchDomain; the probe itself just seeks the goal.

Equations

• c.goalProbe = Minimalist.Probe.ofVis fun (y : Minimalist.SyntacticObject) => decide (y = c.goalHead)

theorem Amato2025.NestedAgree.runStack_eq_search (c : NestedAgreeConfig) (i : ℕ) : runStack c i = if i < c.length then c.goalProbe.search (c.searchDomain i).toList else none

runStack factors through the canonical Probe.search: running probe i is the goal-seeking probe searching probe i's derived domain (when probe i exists). The bespoke membership test is Probe.search over searchDomain i, bringing Nested Agree onto the one probe engine (cf. CyclicAgree.eaIsLicensed_iff_segment_licensed). The whole-stack composition is findSome?/Probe.cascade over the indices; the per-probe truncated domains are why each step is a search over its own searchDomain, not a cascade over one list.

theorem Amato2025.NestedAgree.goalProbe_licensed_iff (c : NestedAgreeConfig) (i : ℕ) : c.goalProbe.Licensed (c.searchDomain i).toList c.goalHead ↔ c.goalHead ∈ c.searchDomain i

The Nested-Agree licensing fact in the licensing API: probe i licenses the shared goal iff the goal is in probe i's domain.

@[simp]

theorem Amato2025.NestedAgree.searchDomain_succ (c : NestedAgreeConfig) (i : ℕ) : c.searchDomain (i + 1) = c.daughters

Post-initial search domains equal daughters by definition.

theorem Amato2025.NestedAgree.goalHead_mem_daughters (c : NestedAgreeConfig) (h : IsNestedAgreeConfig c) : c.goalHead ∈ c.daughters

A well-formed configuration's goal lies in its own daughters (reflexive inclusion + phi-active). Used in the apparent-minimality theorem.

theorem Amato2025.NestedAgree.apparent_intervener_excluded (c : NestedAgreeConfig) (i : ℕ) (δ : Minimalist.SyntacticObject) (hVisible : δ ∈ c.initialDomain) (hOut : δ ∉ c.daughters) : δ ∈ c.searchDomain 0 ∧ δ ∉ c.searchDomain (i + 1)

A subtree visible to probe 0 but outside daughters is excluded from every post-initial probe's search domain. Strict-truncation content in the conclusion's ∈ ∧ ∉ shape.

theorem Amato2025.NestedAgree.apparent_minimality_not_actual (c : NestedAgreeConfig) (h : IsNestedAgreeConfig c) (i : ℕ) (δ : Minimalist.SyntacticObject) (hOut : δ ∉ c.daughters) : runStack c (i + 1) ≠ some δ

A subtree outside the goal's daughters cannot be returned by any post-initial probe — runStack only ever produces the (well- formedness-guaranteed) goalHead, which by goalHead_mem_daughters is inside its own daughters.

Standard linear-Spec configuration builder

The four landed Amato 2025 case studies (Italian aux, Icelandic DAT-NOM, Lak perfective, Bulgarian wh) all share a structural template: a 4-leaf binary tree [probe-head [intervener [mid goal]]] with a 2-probe stack on the head. The builder below extracts this template so consumers don't repeat it.

Consumers vary in:

• LIToken category labels (T / C / Asp; DPsubj / DPdat / Erg / WhSbj; V; DPobj / DPnom / Abs / WhObj)
• Which leaf is the chosen goal (typically midNode in Italian/Lak, terminal in Icelandic/Bulgarian)
• The validGoal predicate

The common shape — a single Probe.Profile used twice, a 4-leaf linear tree, the 2-probe stack — is captured by standardConfig.

def Amato2025.NestedAgree.standardLinearTree (probeHd intervener midNode terminal : Minimalist.LIToken) : Minimalist.SyntacticObject

Standard 4-leaf linear-Spec tree: [probeHd [intervener [midNode terminal]]]. Shared template across the landed Amato 2025 case studies.

Equations

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

def Amato2025.NestedAgree.standardConfig (probeProfile : Minimalist.Probe.Profile) (probeHd intervener midNode terminal goalHd : Minimalist.LIToken) (vg : Minimalist.SyntacticObject → Bool) : NestedAgreeConfig

A NestedAgreeConfig over the standard linear tree, with a 2-probe stack on probeHd. The goalHd selects which leaf serves as the shared goal under maximized matching.

Equations

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

A 2-probe stack on a Perf+vP SyntacticObject

Tree: Perf [DPsubj [v DPobj]]. Probe 0 (Infl-Agree) targets v; probe 1 (π-Agree) is restricted by Nested Agree to v's c-command domain (reflexively including v). The apparent intervener DPsubj is in Perf's c-command but not in v's, so it is structurally excluded from probe 1 — encoding [Ama25]'s resolution of the apparent minimality violation.

validGoal is true everywhere here (transitive case); the unaccusative case (validGoal (SO.lexLeaf aV) = false) is the one tested in Studies/Amato2025.lean.

def Amato2025.NestedAgree.italianAuxExample : NestedAgreeConfig

Italian-style 2-probe configuration constructed via standardConfig.

Equations

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

theorem Amato2025.NestedAgree.italianAuxExample_is_nested : IsNestedAgreeConfig italianAuxExample

theorem Amato2025.NestedAgree.italianAuxExample_runStack_0 : runStack italianAuxExample 0 = some (Minimalist.SO.lexLeaf Amato2025.NestedAgree.aV✝)

theorem Amato2025.NestedAgree.italianAuxExample_runStack_1 : runStack italianAuxExample 1 = some (Minimalist.SO.lexLeaf Amato2025.NestedAgree.aV✝)

theorem Amato2025.NestedAgree.italianAuxExample_excludes_apparent_intervener : Minimalist.SO.lexLeaf Amato2025.NestedAgree.aDPsubj✝ ∈ italianAuxExample.searchDomain 0 ∧ Minimalist.SO.lexLeaf Amato2025.NestedAgree.aDPsubj✝ ∉ italianAuxExample.searchDomain 1

DPsubj is in probe 0's c-command (Perf c-commands DPsubj) but not in probe 1's truncated domain (v doesn't c-command DPsubj). Real strict-truncation content from the Minimalist c-command primitive.