Sluicing: Syntactic Isomorphism Condition

Formalization of @cite{anand-hardt-mccloskey-2025} Syntactic Isomorphism Condition for sluicing, building on @cite{grimshaw-2005} Extended Projection, with a comparison to @cite{rudin-2019}'s domination-chain–based structure matching.

Key Ideas

Sluicing is licensed when the argument domain of the ellipsis site is structurally identical to the argument domain of the antecedent.

1. Argument Domain (Def 4): The most inclusive projection in an EP that denotes type ⟨e,t⟩ (property). For full clauses, this is vP.
2. Head Pair (Def 5): A pair ⟨head, complement⟩ within the argument domain, encoding local syntactic structure.
3. Structural Identity (Def 6): Two argument domains are structurally identical iff their head pairs can be put in 1-1 correspondence with lexical identity.
4. SIC: Sluicing is licensed iff structural identity holds between antecedent and ellipsis argument domains.

Predictions

• Voice mismatch: v[agentive] ≠ v[nonThematic] within argument domain → SIC violation
• Case matching: Case is assigned within the argument domain → must match
• Small clause antecedents: Smaller argument domain → more permissive matching
• Copular pseudosluices: AHM licenses (head pairs match); Rudin blocks (domain roots differ: SC .N ≠ DP .D)

AHM vs Rudin

@cite{rudin-2019} Def 9 requires domination chains from the domain root to match. This makes the domain root category load-bearing. @cite{anand-hardt-mccloskey-2025} Def 6 checks only head pairs, abstracting away from the domain root. The theories converge on standard sluicing (same domain root) and diverge on cross-category antecedence (different domain roots). We prove this convergence/divergence generally via same_root_convergence.

structure Minimalist.Ellipsis.FormalMatching.HeadPair : Type

A head pair: a head and its complement category within the argument domain. Head pairs encode the local syntactic structure that must match between antecedent and ellipsis site.

@cite{anand-hardt-mccloskey-2025} Definition 5: Two heads are lexically identical iff they have the same category AND complement category. Case is included because it is assigned within the argument domain: a V that assigns dative is structurally distinct from one that assigns accusative (@cite{merchant-2001}, @cite{anand-hardt-mccloskey-2021} §5.5).

• head : Cat

  The category of the head

• complement : Cat

  The category of its complement

• assignedCase : Option UD.Case

  Case assigned by the head to its complement, when relevant. none for head pairs where case is not assigned (e.g., v–V).

• voiceFlavor : Option VoiceFlavor

  Voice flavor of the head (agentive, nonThematic, etc.), when relevant. Distinguishes active v[agentive] from passive v[nonThematic] within the argument domain.

• isArgumentPP : Option Bool

  Is this PP an argument of the verb (selected) or an adjunct? @cite{anand-hardt-mccloskey-2025} §4: argument PPs (e.g., "rely on X") are inside the argument domain and must match under the SIC; nonargument PPs (e.g., "sing in the shower") are outside. none for non-PP head pairs.

def Minimalist.Ellipsis.FormalMatching.instReprHeadPair.repr : HeadPair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instReprHeadPair : Repr HeadPair

Equations

• Minimalist.Ellipsis.FormalMatching.instReprHeadPair = { reprPrec := Minimalist.Ellipsis.FormalMatching.instReprHeadPair.repr }

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableEqHeadPair : DecidableEq HeadPair

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableEqHeadPair = Minimalist.Ellipsis.FormalMatching.instDecidableEqHeadPair.decEq

def Minimalist.Ellipsis.FormalMatching.instDecidableEqHeadPair.decEq (x✝ x✝¹ : HeadPair) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Ellipsis.FormalMatching.optAgree {α : Type} [DecidableEq α] (o1 o2 : Option α) : Prop

Optional-field "agreement" predicate: two Option α values agree iff either is none, or both are some with equal contents. Used by lexicallyIdentical (and rudinIdentical below) to model "match the field if both sides specify it."

Equations

• Minimalist.Ellipsis.FormalMatching.optAgree o1 o2 = (o1.isNone = true ∨ o2.isNone = true ∨ o1 = o2)

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableOptAgree {α : Type} [DecidableEq α] (o1 o2 : Option α) : Decidable (optAgree o1 o2)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableOptAgree o1 o2 = id inferInstance

def Minimalist.Ellipsis.FormalMatching.lexicallyIdentical (hp1 hp2 : HeadPair) : Prop

Lexical identity of head pairs (@cite{anand-hardt-mccloskey-2025}, Def 5): Two head pairs are lexically identical iff they have the same head category, complement category, and assigned case (when both specify case).

Case matching follows from the SIC because case is assigned within the argument domain: if the head assigns different case, the head-complement relationship is structurally distinct.

When either side has assignedCase = none, case is not checked (the head pair does not involve case assignment, e.g., v selecting VP).

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableLexicallyIdentical (hp1 hp2 : HeadPair) : Decidable (lexicallyIdentical hp1 hp2)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableLexicallyIdentical hp1 hp2 = id inferInstance

def Minimalist.Ellipsis.FormalMatching.removeFirst {α : Type} (p : α → Prop) [DecidablePred p] : List α → Option (List α)

Remove the first element matching a decidable predicate from a list. Returns none if no match found, some remaining otherwise.

Polymorphic over (α → Prop) with [DecidablePred p] so that consumers can pass Prop predicates (e.g., lexicallyIdentical hp) directly without Bool wrapping.

Equations

• Minimalist.Ellipsis.FormalMatching.removeFirst p [] = none
• Minimalist.Ellipsis.FormalMatching.removeFirst p (x_1 :: xs) = if p x_1 then some xs else Option.map (fun (x : List α) => x_1 :: x) (Minimalist.Ellipsis.FormalMatching.removeFirst p xs)

def Minimalist.Ellipsis.FormalMatching.matchHeadPairs : List HeadPair → List HeadPair → Prop

Check if every head pair in pairs1 has a lexically identical match in pairs2, consuming matches (1-1 correspondence).

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Ellipsis.FormalMatching.matchHeadPairs [] x✝ = True

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableMatchHeadPairs (l1 l2 : List HeadPair) : Decidable (matchHeadPairs l1 l2)

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Ellipsis.FormalMatching.instDecidableMatchHeadPairs [] x✝ = isTrue trivial

def Minimalist.Ellipsis.FormalMatching.structurallyIdentical (pairs1 pairs2 : List HeadPair) : Prop

Structural identity (@cite{anand-hardt-mccloskey-2025}, Def 6): Two sets of head pairs are structurally identical iff they can be put in 1-1 correspondence where each pair is lexically identical.

This requires same cardinality AND a bijective matching.

Equations

• Minimalist.Ellipsis.FormalMatching.structurallyIdentical pairs1 pairs2 = (pairs1.length = pairs2.length ∧ Minimalist.Ellipsis.FormalMatching.matchHeadPairs pairs1 pairs2)

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableStructurallyIdentical (pairs1 pairs2 : List HeadPair) : Decidable (structurallyIdentical pairs1 pairs2)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableStructurallyIdentical pairs1 pairs2 = id inferInstance

structure Minimalist.Ellipsis.FormalMatching.SluicingLicense : Type

Sluicing license: the Syntactic Isomorphism Condition (SIC).

Sluicing of a CP is licensed iff the argument domain of the ellipsis site has structurally identical head pairs to the argument domain of the antecedent.

• antecedentPairs : List HeadPair

  Head pairs from the antecedent's argument domain

• ellipsisPairs : List HeadPair

  Head pairs from the ellipsis site's argument domain

def Minimalist.Ellipsis.FormalMatching.SluicingLicense.isLicensed (sl : SluicingLicense) : Prop

Is sluicing licensed? Checks structural identity of head pairs.

Equations

• sl.isLicensed = Minimalist.Ellipsis.FormalMatching.structurallyIdentical sl.antecedentPairs sl.ellipsisPairs

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableIsLicensed (sl : SluicingLicense) : Decidable sl.isLicensed

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableIsLicensed sl = id inferInstance

theorem Minimalist.Ellipsis.FormalMatching.voice_flavor_in_argdomain : isInArgumentDomain Cat.Voice Cat.C = true

Voice is within the argument domain (F1, same level as v). @cite{anand-hardt-mccloskey-2021}: voice mismatches ARE blocked by the SIC because v[agentive] ≠ v[nonThematic] within the argument domain.

theorem Minimalist.Ellipsis.FormalMatching.t_outside_argdomain : isInArgumentDomain Cat.T Cat.C = false

T is not within the argument domain of a CP.

theorem Minimalist.Ellipsis.FormalMatching.c_outside_argdomain : isInArgumentDomain Cat.C Cat.C = false

C is not within the argument domain.

def Minimalist.Ellipsis.FormalMatching.activeVP : List HeadPair

Head pairs for an active (agentive) transitive vP. v[agentive] selects VP, V selects DP.

Equations

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

def Minimalist.Ellipsis.FormalMatching.passiveVP : List HeadPair

Head pairs for a passive (non-thematic) transitive vP. v[nonThematic] selects VP, V selects DP.

Equations

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

theorem Minimalist.Ellipsis.FormalMatching.voice_mismatch_blocks_sluicing : ¬structurallyIdentical activeVP passiveVP

Voice mismatch blocks sluicing: active v[agentive] ≠ passive v[nonThematic] within the argument domain.

theorem Minimalist.Ellipsis.FormalMatching.voice_match_licenses_sluicing : structurallyIdentical activeVP activeVP

Same voice licenses sluicing: active→active is structurally identical.

theorem Minimalist.Ellipsis.FormalMatching.v_lexical_in_argdomain : isInArgumentDomain Cat.V Cat.C = true

V is within the argument domain of a CP (F0 ≤ F1).

theorem Minimalist.Ellipsis.FormalMatching.v_functional_in_argdomain : isInArgumentDomain Cat.v Cat.C = true

v is within the argument domain of a CP (F1 ≤ F1).

theorem Minimalist.Ellipsis.FormalMatching.small_clause_argdomain_is_self : argumentDomainCat Cat.V = Cat.V

For a small clause (top = V), the argument domain is V itself. Only F0 heads are in the argument domain.

theorem Minimalist.Ellipsis.FormalMatching.small_clause_excludes_v : isInArgumentDomain Cat.v Cat.V = false

In a small clause, v is NOT in the argument domain (since the top is V at F0, and v is F1).

theorem Minimalist.Ellipsis.FormalMatching.sc_P_argdomain_is_self : argumentDomainCat Cat.P = Cat.P

For a P-headed small clause, the argument domain is P itself. E.g., absolute with: "with [the campaign on hold]".

theorem Minimalist.Ellipsis.FormalMatching.sc_A_argdomain_is_self : argumentDomainCat Cat.A = Cat.A

For an A-headed small clause, the argument domain is A itself. E.g., resultative: "hammer [the metal flat]".

theorem Minimalist.Ellipsis.FormalMatching.sc_N_argdomain_is_self : argumentDomainCat Cat.N = Cat.N

For an N-headed small clause, the argument domain is N itself. E.g., copular: "consider [John a fool]".

def Minimalist.Ellipsis.FormalMatching.scArgumentDomainCat (sc : SCPredCategory) : Cat

The argument domain boundary for an SC is the SC predicate category.

Equations

• Minimalist.Ellipsis.FormalMatching.scArgumentDomainCat sc = Minimalist.argumentDomainCat sc.toCat

theorem Minimalist.Ellipsis.FormalMatching.sc_argdomain_at_f0 (sc : SCPredCategory) : fValue (scArgumentDomainCat sc) = 0

SC argument domains are uniformly at F0 (lexical level).

theorem Minimalist.Ellipsis.FormalMatching.sc_argdomain_le_clause (sc : SCPredCategory) : fValue (scArgumentDomainCat sc) ≤ fValue (argumentDomainCat Cat.C)

SC argument domains are smaller than full clause argument domains.

def Minimalist.Ellipsis.FormalMatching.scHeadPairsForCat (cat : SCPredCategory) : List HeadPair

Head pairs from a small clause's argument domain. The SC argument domain contains only the predicate head and its complement (the subject DP), yielding a single head pair.

Equations

• Minimalist.Ellipsis.FormalMatching.scHeadPairsForCat cat = [{ head := cat.toCat, complement := Minimalist.Cat.D }]

theorem Minimalist.Ellipsis.FormalMatching.sc_sic_fewer_constraints : (scHeadPairsForCat SCPredCategory.A).length < activeVP.length

SC sluicing requires fewer matches than full-clause sluicing.

theorem Minimalist.Ellipsis.FormalMatching.sc_same_pred_sluicing_licensed (cat : SCPredCategory) : structurallyIdentical (scHeadPairsForCat cat) (scHeadPairsForCat cat)

SIC licenses SC sluicing when antecedent and ellipsis share the same SC predicate category (same ⟨PredCat, D⟩ head pair).

theorem Minimalist.Ellipsis.FormalMatching.lexicallyIdentical_refl (hp : HeadPair) : lexicallyIdentical hp hp

Lexical identity is reflexive for any head pair.

theorem Minimalist.Ellipsis.FormalMatching.removeFirst_self (hp : HeadPair) (rest : List HeadPair) : removeFirst (lexicallyIdentical hp) (hp :: rest) = some rest

Removing the first lexically identical element from a list headed by that element succeeds and returns the tail.

theorem Minimalist.Ellipsis.FormalMatching.matchHeadPairs_refl (pairs : List HeadPair) : matchHeadPairs pairs pairs

Head pair matching is reflexive: any list matches itself.

theorem Minimalist.Ellipsis.FormalMatching.structurallyIdentical_refl (pairs : List HeadPair) : structurallyIdentical pairs pairs

Structural identity is reflexive: any set of head pairs is structurally identical to itself. This subsumes empty_domains_identical and single_pair_matches.

theorem Minimalist.Ellipsis.FormalMatching.empty_domains_identical : structurallyIdentical [] []

Empty argument domains are trivially structurally identical.

theorem Minimalist.Ellipsis.FormalMatching.single_pair_matches (hp : HeadPair) : structurallyIdentical [hp] [hp]

A single head pair matches itself.

theorem Minimalist.Ellipsis.FormalMatching.case_mismatch_not_identical : ¬lexicallyIdentical { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat } { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Acc }

Case mismatch blocks lexical identity: a V–D pair assigning dative is not lexically identical to one assigning accusative.

theorem Minimalist.Ellipsis.FormalMatching.case_match_identical : lexicallyIdentical { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat } { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }

Case match preserves lexical identity.

theorem Minimalist.Ellipsis.FormalMatching.no_case_identity : lexicallyIdentical { head := Cat.v, complement := Cat.V } { head := Cat.v, complement := Cat.V }

When no case is specified (e.g., v–V), identity depends only on categories.

theorem Minimalist.Ellipsis.FormalMatching.case_mismatch_blocks_sluicing : ¬structurallyIdentical [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }] [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Acc }]

Case mismatch blocks structural identity even when all other head pairs match. This is the formal basis of the German case-matching data: "wem" (dat) matches "jemandem" (dat), but "wen" (acc) does not.

theorem Minimalist.Ellipsis.FormalMatching.case_match_licenses_sluicing : structurallyIdentical [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }] [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }]

Same case → structural identity holds → sluicing licensed.

structure Minimalist.Ellipsis.FormalMatching.VerbFrame : Type

A verb frame specifies the derivation-level properties of a verbal structure that are relevant for the SIC.

Each frame corresponds to a well-formed Minimalist derivation [vP v[voice] [VP V complement]], where v selects VP and V selects a DP or PP complement. The SIC compares the head pairs extracted from the argument domain of such derivations.

This connects the SIC to the Minimalist machinery: head pairs are not stipulated but arise from structured derivation specs that correspond to concrete SyntacticObject trees.

• voice : VoiceFlavor

  Voice flavor of the v head

• objectCase : Option UD.Case

  Case assigned by V to its complement (when relevant)

• argumentPP : Bool

  Does V select an argument PP rather than a DP complement?

def Minimalist.Ellipsis.FormalMatching.instReprVerbFrame.repr : VerbFrame → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instReprVerbFrame : Repr VerbFrame

Equations

• Minimalist.Ellipsis.FormalMatching.instReprVerbFrame = { reprPrec := Minimalist.Ellipsis.FormalMatching.instReprVerbFrame.repr }

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableEqVerbFrame : DecidableEq VerbFrame

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableEqVerbFrame = Minimalist.Ellipsis.FormalMatching.instDecidableEqVerbFrame.decEq

def Minimalist.Ellipsis.FormalMatching.instDecidableEqVerbFrame.decEq (x✝ x✝¹ : VerbFrame) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Ellipsis.FormalMatching.VerbFrame.headPairs (vf : VerbFrame) : List HeadPair

Head pairs extracted from a verb frame's argument domain. The argument domain for a clausal derivation is vP, containing:

• ⟨v, V⟩: the v head selecting VP (annotated with voice flavor)
• ⟨V, D/P⟩: the V head selecting its complement (annotated with case)

Equations

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

def Minimalist.Ellipsis.FormalMatching.VerbFrame.tree (vf : VerbFrame) (vId verbId complId : ℕ) : SyntacticObject

Build a concrete SyntacticObject tree from a verb frame. Produces the tree [vP v [VP V DP/PP]]:

• v (sel: [V]) — little v, selects VP
• V (sel: [D] or [P]) — lexical verb, selects complement
• DP/PP (sel: []) — complement

Equations

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

def Minimalist.Ellipsis.FormalMatching.activeFrame : VerbFrame

Active transitive: v[agentive] selects VP, V selects DP.

Equations

• Minimalist.Ellipsis.FormalMatching.activeFrame = { voice := Minimalist.VoiceFlavor.agentive }

def Minimalist.Ellipsis.FormalMatching.passiveFrame : VerbFrame

Passive transitive: v[nonThematic] selects VP, V selects DP.

Equations

• Minimalist.Ellipsis.FormalMatching.passiveFrame = { voice := Minimalist.VoiceFlavor.nonThematic }

def Minimalist.Ellipsis.FormalMatching.dativeFrame : VerbFrame

Dative verb (e.g., German "helfen"): V assigns dative case.

Equations

• Minimalist.Ellipsis.FormalMatching.dativeFrame = { voice := Minimalist.VoiceFlavor.agentive, objectCase := some UD.Case.Dat }

def Minimalist.Ellipsis.FormalMatching.accusativeFrame : VerbFrame

Accusative verb (e.g., German "sehen"): V assigns accusative case.

Equations

• Minimalist.Ellipsis.FormalMatching.accusativeFrame = { voice := Minimalist.VoiceFlavor.agentive, objectCase := some UD.Case.Acc }

def Minimalist.Ellipsis.FormalMatching.argumentPPFrame : VerbFrame

Argument PP verb (e.g., "rely on"): V selects a PP complement.

Equations

• Minimalist.Ellipsis.FormalMatching.argumentPPFrame = { voice := Minimalist.VoiceFlavor.agentive, argumentPP := true }

theorem Minimalist.Ellipsis.FormalMatching.activeFrame_eq : activeFrame.headPairs = activeVP

Active frame head pairs match the hand-specified activeVP.

theorem Minimalist.Ellipsis.FormalMatching.passiveFrame_eq : passiveFrame.headPairs = passiveVP

Passive frame head pairs match the hand-specified passiveVP.

def Minimalist.Ellipsis.FormalMatching.frameSluicingLicensed (antecedent ellipsis : VerbFrame) : Prop

Is sluicing licensed between two verb frames? Checks structural identity of their argument domain head pairs.

Equations

• Minimalist.Ellipsis.FormalMatching.frameSluicingLicensed antecedent ellipsis = Minimalist.Ellipsis.FormalMatching.structurallyIdentical antecedent.headPairs ellipsis.headPairs

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableFrameSluicingLicensed (a e : VerbFrame) : Decidable (frameSluicingLicensed a e)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableFrameSluicingLicensed a e = id inferInstance

theorem Minimalist.Ellipsis.FormalMatching.same_frame_always_licensed (vf : VerbFrame) : frameSluicingLicensed vf vf

Any verb frame is structurally identical to itself. This is non-trivial: it says that 1-1 head pair matching succeeds reflexively, regardless of voice, case, and argument type.

theorem Minimalist.Ellipsis.FormalMatching.voice_determines_v_pair (v : VoiceFlavor) (c1 c2 : Option UD.Case) (pp1 pp2 : Bool) : { voice := v, objectCase := c1, argumentPP := pp1 }.headPairs.head? = { voice := v, objectCase := c2, argumentPP := pp2 }.headPairs.head?

The v–V head pair depends only on voice flavor: two frames with the same voice produce identical first head pairs, regardless of case or argument type.

theorem Minimalist.Ellipsis.FormalMatching.voice_mismatch_from_frames : ¬frameSluicingLicensed activeFrame passiveFrame

Voice mismatch blocks sluicing, derived from frames. Proof: unfold to head pairs, then activeFrame_eq/passiveFrame_eq reduce to the known voice_mismatch_blocks_sluicing.

theorem Minimalist.Ellipsis.FormalMatching.case_mismatch_from_frames : ¬frameSluicingLicensed dativeFrame accusativeFrame

Case mismatch blocks sluicing, derived from frames.

theorem Minimalist.Ellipsis.FormalMatching.same_case_from_frames : frameSluicingLicensed dativeFrame dativeFrame

Same-case frames are licensed.

def Minimalist.Ellipsis.FormalMatching.crossCategorySluicing (vf : VerbFrame) (sc : SCPredCategory) : Prop

Is sluicing licensed between a verb frame and an SC frame? Cross-category sluicing (full clause ↔ SC) involves different argument domain sizes, so it typically fails the SIC.

Equations

• Minimalist.Ellipsis.FormalMatching.crossCategorySluicing vf sc = Minimalist.Ellipsis.FormalMatching.structurallyIdentical vf.headPairs (Minimalist.Ellipsis.FormalMatching.scHeadPairsForCat sc)

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableCrossCategorySluicing (vf : VerbFrame) (sc : SCPredCategory) : Decidable (crossCategorySluicing vf sc)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableCrossCategorySluicing vf sc = id inferInstance

theorem Minimalist.Ellipsis.FormalMatching.cross_category_blocked (vf : VerbFrame) (sc : SCPredCategory) : ¬crossCategorySluicing vf sc

Full clause → SC cross-category sluicing fails: different numbers of head pairs (2 vs 1) means the SIC length check blocks.

theorem Minimalist.Ellipsis.FormalMatching.verbframe_argdomain_wellformed : categoryConsistent Cat.V Cat.v = true ∧ fMonotone Cat.V Cat.v = true

The argument domain spine for any verb frame is [V, v], which is F-monotone and category-consistent.

theorem Minimalist.Ellipsis.FormalMatching.verbframe_argdomain_complete : isInArgumentDomain Cat.V Cat.C = true ∧ isInArgumentDomain Cat.v Cat.C = true ∧ isInArgumentDomain Cat.T Cat.C = false ∧ isInArgumentDomain Cat.C Cat.C = false

The verbal argument domain contains exactly F0 (.V) and F1 (.v). Everything above (T, C, Mod, ...) is outside.

def Minimalist.Ellipsis.FormalMatching.HeadPair.isNonargumentPP (hp : HeadPair) : Bool

Is this head pair a nonargument PP? Nonargument PPs are outside the argument domain: they are merged above vP and do not participate in the SIC matching calculation.

@cite{anand-hardt-mccloskey-2025} §4: Chung's Generalization (preposition stranding in sluicing) follows because stranded prepositions in nonargument PPs need not match structurally.

Equations

• hp.isNonargumentPP = (hp.head == Minimalist.Cat.P && hp.isArgumentPP == some false)

def Minimalist.Ellipsis.FormalMatching.filterArgumentPairs (pairs : List HeadPair) : List HeadPair

Filter head pairs to only those within the argument domain, excluding nonargument PPs. The SIC applies to the filtered list.

Equations

• Minimalist.Ellipsis.FormalMatching.filterArgumentPairs pairs = List.filter (fun (hp : Minimalist.Ellipsis.FormalMatching.HeadPair) => !hp.isNonargumentPP) pairs

theorem Minimalist.Ellipsis.FormalMatching.chung_generalization : have antecedent := [{ head := Cat.v, complement := Cat.V, voiceFlavor := some VoiceFlavor.agentive }, { head := Cat.V, complement := Cat.D }]; have ellipsis := [{ head := Cat.v, complement := Cat.V, voiceFlavor := some VoiceFlavor.agentive }, { head := Cat.V, complement := Cat.D }, { head := Cat.P, complement := Cat.D, isArgumentPP := some false }]; structurallyIdentical (filterArgumentPairs antecedent) (filterArgumentPairs ellipsis)

Chung's Generalization: a stranded nonargument preposition in the ellipsis site need not have a counterpart in the antecedent.

@cite{anand-hardt-mccloskey-2025} §4: "government regulation is necessary in [some form]" — the stranded in has no antecedent source, but sluicing is licensed because the PP is nonargument (outside the argument domain). Filtering removes it, and the remaining argument-domain head pairs match.

theorem Minimalist.Ellipsis.FormalMatching.argument_pp_must_match : have vp1 := [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.P, isArgumentPP := some true }]; have vp2 := [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.P, isArgumentPP := some true }]; structurallyIdentical (filterArgumentPairs vp1) (filterArgumentPairs vp2) = (true = true)

An argument PP (selected by V) IS inside the argument domain and DOES require matching. "I rely on her" vs "I rely at her" — case is wrong, and the PP is argument-marking, so SIC blocks.

structure Minimalist.Ellipsis.FormalMatching.DomainAnnotatedPair : Type

@cite{rudin-2019}'s structure matching (Def 9) requires that heads be dominated by identical sequences of immediately dominating nodes. This means the domain root category is necessarily part of the match: every domination chain starts from the domain root.

@cite{anand-hardt-mccloskey-2025}'s SIC (Def 6) checks only head pairs ⟨head, complement⟩ within the argument domain, without reference to the domain root.

We capture this difference by annotating each head pair with its domain root category. Rudin's condition requires domain root identity; AHM's condition ignores it. This is a deliberate simplification of the full domination-chain machinery — we abstract to the single feature (domain root) that drives the empirical divergence.

• pair : HeadPair

  The head pair within the argument domain

• domainRoot : Cat

  The root category of the domain containing this head pair. For full clauses: .v (vP argument domain). For N-headed SCs: .N. For DPs: .D.

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instReprDomainAnnotatedPair : Repr DomainAnnotatedPair

Equations

• Minimalist.Ellipsis.FormalMatching.instReprDomainAnnotatedPair = { reprPrec := Minimalist.Ellipsis.FormalMatching.instReprDomainAnnotatedPair.repr }

def Minimalist.Ellipsis.FormalMatching.instReprDomainAnnotatedPair.repr : DomainAnnotatedPair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableEqDomainAnnotatedPair : DecidableEq DomainAnnotatedPair

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableEqDomainAnnotatedPair = Minimalist.Ellipsis.FormalMatching.instDecidableEqDomainAnnotatedPair.decEq

def Minimalist.Ellipsis.FormalMatching.instDecidableEqDomainAnnotatedPair.decEq (x✝ x✝¹ : DomainAnnotatedPair) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Ellipsis.FormalMatching.annotateWithRoot (root : Cat) (pairs : List HeadPair) : List DomainAnnotatedPair

Annotate a list of head pairs with a uniform domain root category. Used to lift AHM-style head pairs into Rudin-style annotated pairs.

Equations

• Minimalist.Ellipsis.FormalMatching.annotateWithRoot root pairs = List.map (fun (x : Minimalist.Ellipsis.FormalMatching.HeadPair) => { pair := x, domainRoot := root }) pairs

def Minimalist.Ellipsis.FormalMatching.rudinIdentical (h1 h2 : DomainAnnotatedPair) : Prop

Rudin-style matching: lexical identity of head pairs PLUS domain root identity. The domain root requirement follows from @cite{rudin-2019} Def 9: domination chains necessarily include the domain root as their first element, so if domain roots differ, no chain can match.

Equations

• Minimalist.Ellipsis.FormalMatching.rudinIdentical h1 h2 = (Minimalist.Ellipsis.FormalMatching.lexicallyIdentical h1.pair h2.pair ∧ h1.domainRoot = h2.domainRoot)

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableRudinIdentical (h1 h2 : DomainAnnotatedPair) : Decidable (rudinIdentical h1 h2)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableRudinIdentical h1 h2 = id inferInstance

def Minimalist.Ellipsis.FormalMatching.rudinMatchPairs : List DomainAnnotatedPair → List DomainAnnotatedPair → Prop

Match head pairs using Rudin's stricter criterion (1-1 correspondence).

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Ellipsis.FormalMatching.rudinMatchPairs [] x✝ = True

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableRudinMatchPairs (l1 l2 : List DomainAnnotatedPair) : Decidable (rudinMatchPairs l1 l2)

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Ellipsis.FormalMatching.instDecidableRudinMatchPairs [] x✝ = isTrue trivial

def Minimalist.Ellipsis.FormalMatching.rudinStructurallyIdentical (pairs1 pairs2 : List DomainAnnotatedPair) : Prop

Rudin's structural identity: same cardinality + Rudin-style matching.

Equations

• Minimalist.Ellipsis.FormalMatching.rudinStructurallyIdentical pairs1 pairs2 = (pairs1.length = pairs2.length ∧ Minimalist.Ellipsis.FormalMatching.rudinMatchPairs pairs1 pairs2)

@[implicit_reducible]

instance Minimalist.Ellipsis.FormalMatching.instDecidableRudinStructurallyIdentical (pairs1 pairs2 : List DomainAnnotatedPair) : Decidable (rudinStructurallyIdentical pairs1 pairs2)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableRudinStructurallyIdentical pairs1 pairs2 = id inferInstance

theorem Minimalist.Ellipsis.FormalMatching.same_root_convergence (pairs1 pairs2 : List HeadPair) (root : Cat) : rudinStructurallyIdentical (annotateWithRoot root pairs1) (annotateWithRoot root pairs2) ↔ structurallyIdentical pairs1 pairs2

When both sides are annotated with the same domain root, Rudin's structural identity is equivalent to AHM's. The theories converge whenever the domain roots match — only differing domain roots can cause divergence (as in copular pseudosluices).

def Minimalist.Ellipsis.FormalMatching.rudinActiveVP : List DomainAnnotatedPair

Active transitive vP annotated with domain root .v

Equations

• Minimalist.Ellipsis.FormalMatching.rudinActiveVP = Minimalist.Ellipsis.FormalMatching.annotateWithRoot Minimalist.Cat.v Minimalist.Ellipsis.FormalMatching.activeVP

def Minimalist.Ellipsis.FormalMatching.rudinPassiveVP : List DomainAnnotatedPair

Passive transitive vP annotated with domain root .v

Equations

• Minimalist.Ellipsis.FormalMatching.rudinPassiveVP = Minimalist.Ellipsis.FormalMatching.annotateWithRoot Minimalist.Cat.v Minimalist.Ellipsis.FormalMatching.passiveVP

theorem Minimalist.Ellipsis.FormalMatching.rudin_also_blocks_voice_mismatch : ¬rudinStructurallyIdentical rudinActiveVP rudinPassiveVP

Convergence: Rudin and AHM agree that voice mismatch blocks sluicing. Both theories: active v[agentive] ≠ passive v[nonThematic]. Derived from same_root_convergence + voice_mismatch_blocks_sluicing.

theorem Minimalist.Ellipsis.FormalMatching.rudin_also_licenses_same_voice : rudinStructurallyIdentical rudinActiveVP rudinActiveVP

Convergence: Rudin and AHM agree that same voice licenses sluicing. Derived from same_root_convergence + voice_match_licenses_sluicing.

theorem Minimalist.Ellipsis.FormalMatching.rudin_also_blocks_case_mismatch : ¬rudinStructurallyIdentical (annotateWithRoot Cat.v [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }]) (annotateWithRoot Cat.v [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Acc }])

Convergence: Rudin and AHM agree on case mismatch blocking. Derived from same_root_convergence + case_mismatch_blocks_sluicing.

def Minimalist.Ellipsis.FormalMatching.copularEllipsisSC : List DomainAnnotatedPair

Copular pseudosluice — ellipsis side. The elided clause is [TP T be [SC subject predicate]], whose argument domain is the N-headed SC (domain root = .N). The single head pair is ⟨N, D⟩ (N head, D complement).

Equations

• Minimalist.Ellipsis.FormalMatching.copularEllipsisSC = [{ pair := { head := Minimalist.Cat.N, complement := Minimalist.Cat.D }, domainRoot := Minimalist.Cat.N }]

def Minimalist.Ellipsis.FormalMatching.copularAntecedentDP : List DomainAnnotatedPair

Copular pseudosluice — antecedent side. The antecedent is a bare DP (e.g., "a presidential race"). Same head pair ⟨N, D⟩, but domain root = .D.

Equations

• Minimalist.Ellipsis.FormalMatching.copularAntecedentDP = [{ pair := { head := Minimalist.Cat.N, complement := Minimalist.Cat.D }, domainRoot := Minimalist.Cat.D }]

theorem Minimalist.Ellipsis.FormalMatching.ahm_licenses_copular_pseudosluice : structurallyIdentical [{ head := Cat.N, complement := Cat.D }] [{ head := Cat.N, complement := Cat.D }]

@cite{anand-hardt-mccloskey-2025} correctly licenses copular pseudosluices: the head pair ⟨N, D⟩ in the SC argument domain matches the head pair ⟨N, D⟩ in the antecedent DP. Domain root categories (.N vs .D) are NOT part of AHM's matching.

theorem Minimalist.Ellipsis.FormalMatching.rudin_blocks_copular_pseudosluice : ¬rudinStructurallyIdentical copularEllipsisSC copularAntecedentDP

@cite{rudin-2019}'s condition incorrectly blocks copular pseudosluices: the domain roots differ (.N for the SC, .D for the antecedent DP), so domination chains cannot match.

This is the central empirical argument in @cite{anand-hardt-mccloskey-2025} §5 for revising Rudin's condition. The copular pseudosluice data (23 corpus instances, ex. 18–19) show that a head-pair–based SIC is empirically superior to a domination-chain–based one.

theorem Minimalist.Ellipsis.FormalMatching.copular_pseudosluice_divergence : structurallyIdentical [{ head := Cat.N, complement := Cat.D }] [{ head := Cat.N, complement := Cat.D }] ∧ ¬rudinStructurallyIdentical copularEllipsisSC copularAntecedentDP

The theories diverge on copular pseudosluices: AHM licenses them, Rudin blocks them. The divergence arises because AHM's SIC checks only head pairs (domain-root-invariant), while Rudin's checks domination chains (domain-root-sensitive).

@cite{anand-hardt-mccloskey-2025} ex. 18–19: "Bradley said that he has not shut the door to [a presidential race], though he would not say when." — grammatical, with nominal antecedent and implicit copular elided clause.

theorem Minimalist.Ellipsis.FormalMatching.domain_root_is_divergence_source : rudinStructurallyIdentical rudinActiveVP rudinActiveVP ∧ ¬rudinStructurallyIdentical copularEllipsisSC copularAntecedentDP ∧ structurallyIdentical [{ head := Cat.N, complement := Cat.D }] [{ head := Cat.N, complement := Cat.D }]

The source of divergence: Rudin's matching is sensitive to the domain root category; AHM's is not. When domain roots differ (cross-category antecedence: SC ↔ DP), only AHM's SIC succeeds. When domain roots are the same (standard sluicing: vP ↔ vP), both theories make identical predictions.

noncomputable def Minimalist.Ellipsis.FormalMatching.maximalProjections (h : HeadFunction) (root : SyntacticObject) : Multiset SyntacticObject

Maximal projections within a SO root: subtrees t such that Labeling.isMaximalAt h root t under head function h. Per @cite{bruening-2021} §5.5 ex. 122, the identity condition quantifies over these XPs (modulo movement non-heads).

Parametric over h : HeadFunction per @cite{marcolli-chomsky-berwick-2025} §1.13.6 — there is no canonical "the" labeling without a chosen head function.

Equations

• Minimalist.Ellipsis.FormalMatching.maximalProjections h root = Multiset.filter (fun (t : Minimalist.SyntacticObject) => decide (Minimalist.Labeling.isMaximalAt h root t) = true) root.subtrees

def Minimalist.Ellipsis.FormalMatching.isNonHeadMemberOfChain (x : SyntacticObject) : Bool

A SO is a "nonhead member of a movement chain" iff it is a trace (lower copy left after movement). Per @cite{bruening-2021} §5.5 ex. 122 "not a nonhead member of a movement chain". For G1 only wh-traces in elided IPs are relevant. Higher copies in head-movement chains are not handled — flag for future ATB / remnant studies.

Equations

• Minimalist.Ellipsis.FormalMatching.isNonHeadMemberOfChain x = (Minimalist.isTrace x).isSome

noncomputable def Minimalist.Ellipsis.FormalMatching.labelPathFromRoot (h : HeadFunction) (root target : SyntacticObject) : Option (List Cat)

Equations

• Minimalist.Ellipsis.FormalMatching.labelPathFromRoot h root target = Minimalist.Ellipsis.FormalMatching.labelPathFromRootPlanar✝ h (Quot.out root) target

noncomputable def Minimalist.Ellipsis.FormalMatching.filteredMaxProjPaths (h : HeadFunction) (root : SyntacticObject) : List (List Cat)

Filtered max-proj paths for a tree under head function h. Each filtered max-proj is paired with its path from the root (= sequence of Labeling.labelVertex values). Movement non-heads (wh-traces and other lower copies) are excluded — exactly Bruening's "not a nonhead member of a movement chain" filter.

Equations

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

def Minimalist.Ellipsis.FormalMatching.bruening2021StructurallyIdentical (h : HeadFunction) (antecedent ellipsis : SyntacticObject) : Prop

@cite{bruening-2021} §5.5 ex. 122 maximal-projection identity condition, parametric over the head function h. Ellipsis of ellipsis given antecedent is licit iff their filtered max-proj path lists are permutations of each other.

Stated as Prop; decidable via List.decidablePerm.

Equations

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

@[implicit_reducible]

noncomputable instance Minimalist.Ellipsis.FormalMatching.instDecidableBruening2021StructurallyIdentical (h : HeadFunction) (a e : SyntacticObject) : Decidable (bruening2021StructurallyIdentical h a e)

Equations

• Minimalist.Ellipsis.FormalMatching.instDecidableBruening2021StructurallyIdentical h a e = id inferInstance

theorem Minimalist.Ellipsis.FormalMatching.bruening2021StructurallyIdentical_refl (h : HeadFunction) (so : SyntacticObject) : bruening2021StructurallyIdentical h so so

The maximal-projection identity condition is reflexive: any SO is structurally identical to itself (under any h).