Economy in PF Reduction

@cite{citko-gracanin-yuksek-2025}

Coordinated wh-questions (CWHs) and coordinated sluices (CSs) are two PF-reduced constructions with wh-phrase remnants. Despite superficial similarity, they differ in structure, derivational cost, and empirical properties. Economy governs the choice between ellipsis and multidominance as the PF reduction mechanism.

Key Claims

1. CWHs use non-bulk-sharing MD: each conjunct CP contains one wh-phrase; functional heads (C, T) are multiply dominated. No ellipsis is involved.

2. CSs use bulk-sharing MD + ellipsis: the entire C' is shared between conjuncts; both wh-phrases originate inside the shared vP. The E-feature on C triggers TP deletion (cf. FeatureVal.ellipsis in Core/Features.lean, which models this E-feature).

3. Economy selects the structure: MD is preferred over ellipsis (fewer operations, fewer lexical items). Bulk-sharing MD is more economical than non-bulk-sharing, but is blocked for CWHs by the MWF parameter. CSs can't have the CWH structure because of Pronunciation Economy.

Empirical Contrasts

• CWHs ban coordination of obligatory wh-arguments; CSs allow it.
• CWHs ban wh-object + wh-adjunct with obligatorily transitive verbs; CSs allow it.
• CWHs only allow nonpaired readings; CSs allow paired readings (with obligatorily transitive verbs) and nonpaired readings (with optionally transitive verbs).

Substrate engagement

• MD primitives (PFReductionMechanism, MDSharing, SharedNode, PFReducedCoordination) are imported from Theories/Syntax/Minimalist/Multidominance.lean (anchored on Citko 2014). They were briefly inlined here while the substrate file was absent; restored to substrate for cross-paper reuse.
• MWF parameter substrate (MWFParameter, PhaseEdge, EdgeAsterisk, MWFViolation, EllipsisRepairsMWF) lives in Typology/Question.lean. Cross-linguistic data (Bulgarian, German, Greek) lives in Phenomena/Questions/MultipleWh.lean. The intra-English variety A/B split — paper-specific to @cite{citko-gracanin-yuksek-2025} — stays here.
• Pronunciation Economy is the per-operation primitive pronunciationEconomy : List PFOperation → Prop from Theories/Syntax/Minimalist/Economy.lean. Paper p. 32 ex (45c) needs per-op vacuity (a derivation with one real deletion + one vacuous deletion violates), which a whole-derivation pfBefore ≠ pfAfter check could not express.
• The CS bulk-sharing structure trivially satisfies @cite{bruening-2021}'s identity condition (Minimalist.Ellipsis.FormalMatching §7), since bulk-sharing means the elided TP literally is the antecedent TP (one node, two parents). Stated as a theorem in §10 below.

Integration

• CSs are coordinated sluices — each conjunct of a CS is a sluice. Bridge theorems connect CS data to Sluicing.lean data structures.
• The MWF parameter connects to Questions/MultipleWh.lean: non-MWF languages (English) ban multiple wh-fronting in questions.
• RNR (§9) demonstrates that economy can force BOTH ellipsis and MD in a single derivation (@cite{belk-neeleman-philip-2023}, @cite{barros-vicente-2011}).

inductive CitkoGracaninYuksek2025.WHCoordType : Type

The two PF-reduced wh-coordination constructions.

• CWH : WHCoordType

  Coordinated wh-question: "What and when did John teach?"

• CS : WHCoordType

  Coordinated sluice: "I forgot what and when."

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprWHCoordType : Repr WHCoordType

Equations

• CitkoGracaninYuksek2025.instReprWHCoordType = { reprPrec := CitkoGracaninYuksek2025.instReprWHCoordType.repr }

def CitkoGracaninYuksek2025.instReprWHCoordType.repr : WHCoordType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqWHCoordType : DecidableEq WHCoordType

Equations

• CitkoGracaninYuksek2025.instDecidableEqWHCoordType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CitkoGracaninYuksek2025.WHCoordDatum : Type

An empirical datum contrasting CWHs and CSs.

• sentence : String
• construction : WHCoordType
• whPhrases : List String
• grammatical : Bool
• notes : String

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprWHCoordDatum : Repr WHCoordDatum

Equations

• CitkoGracaninYuksek2025.instReprWHCoordDatum = { reprPrec := CitkoGracaninYuksek2025.instReprWHCoordDatum.repr }

def CitkoGracaninYuksek2025.instReprWHCoordDatum.repr : WHCoordDatum → ℕ → Std.Format

Equations

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

def CitkoGracaninYuksek2025.cwh_basic : WHCoordDatum

Equations

• CitkoGracaninYuksek2025.cwh_basic = { sentence := "What and when did John teach?", construction := CitkoGracaninYuksek2025.WHCoordType.CWH, whPhrases := ["what", "when"], grammatical := true }

def CitkoGracaninYuksek2025.cwh_obligatory_args_banned : WHCoordDatum

CWHs ban coordination of obligatory wh-arguments (ex 5a).

Equations

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

def CitkoGracaninYuksek2025.cwh_obj_adjunct_banned : WHCoordDatum

CWHs ban wh-object + wh-adjunct with obligatorily transitive verbs (ex 6a). Distinct from (5a): here only one wh-phrase is an obligatory argument; the other is an adjunct. The ban persists because the verb ('buy') is obligatorily transitive.

Equations

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

def CitkoGracaninYuksek2025.cs_basic : WHCoordDatum

Equations

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

def CitkoGracaninYuksek2025.cs_obligatory_args_allowed : WHCoordDatum

CSs allow coordination of obligatory wh-arguments (ex 5b).

Equations

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

def CitkoGracaninYuksek2025.cs_obj_adjunct_allowed : WHCoordDatum

CSs allow wh-object + wh-adjunct coordination (ex 6b).

Equations

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

def CitkoGracaninYuksek2025.whCoordContrastTable : List (WHCoordDatum × Bool)

All CWH/CS empirical contrasts as a single drift-sentry table. Replaces seven trivial rfl readouts (cwh_bans_obligatory_args etc.) with one decide-checked aggregate that catches drift in any row.

Equations

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

theorem CitkoGracaninYuksek2025.whCoordContrastTable_consistent : (whCoordContrastTable.all fun (x : WHCoordDatum × Bool) => match x with | (d, expected) => d.grammatical == expected) = true

inductive CitkoGracaninYuksek2025.ReadingType : Type

Reading type for wh-coordination.

• paired : ReadingType

  Each wh-phrase ranges over a single value (n-tuple as the answer).

• nonpaired : ReadingType

  Each wh-phrase ranges over multiple values (cross-product answer).

def CitkoGracaninYuksek2025.instReprReadingType.repr : ReadingType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprReadingType : Repr ReadingType

Equations

• CitkoGracaninYuksek2025.instReprReadingType = { reprPrec := CitkoGracaninYuksek2025.instReprReadingType.repr }

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqReadingType : DecidableEq ReadingType

Equations

• CitkoGracaninYuksek2025.instDecidableEqReadingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CitkoGracaninYuksek2025.ReadingDatum : Type

Reading availability datum.

• construction : WHCoordType
• reading : ReadingType
• available : Bool
• notes : String

def CitkoGracaninYuksek2025.instReprReadingDatum.repr : ReadingDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprReadingDatum : Repr ReadingDatum

Equations

• CitkoGracaninYuksek2025.instReprReadingDatum = { reprPrec := CitkoGracaninYuksek2025.instReprReadingDatum.repr }

def CitkoGracaninYuksek2025.cwh_nonpaired : ReadingDatum

CWHs: only nonpaired reading available (ex 8a).

Equations

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

def CitkoGracaninYuksek2025.cwh_no_paired : ReadingDatum

CWHs: paired reading unavailable (ex 8a).

Equations

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

def CitkoGracaninYuksek2025.cs_paired : ReadingDatum

CSs: paired reading available with obligatorily transitive verbs (ex 8b). The bulk-sharing CS structure puts both wh-phrases inside a single vP.

Equations

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

def CitkoGracaninYuksek2025.cs_nonpaired : ReadingDatum

CSs: nonpaired reading available with optionally transitive verbs (§6.1, ex 43). With optionally transitive verbs, the CWH-style structure becomes available, yielding a nonpaired reading.

Equations

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

def CitkoGracaninYuksek2025.readingTable : List ReadingDatum

Reading availability drift sentry. Replaces three rfl-readouts.

Equations

• CitkoGracaninYuksek2025.readingTable = [CitkoGracaninYuksek2025.cwh_nonpaired, CitkoGracaninYuksek2025.cwh_no_paired, CitkoGracaninYuksek2025.cs_paired, CitkoGracaninYuksek2025.cs_nonpaired]

theorem CitkoGracaninYuksek2025.readingTable_consistent : cwh_nonpaired.available = true ∧ cwh_no_paired.available = false ∧ cs_paired.available = true ∧ cs_nonpaired.available = true

Drift sentry: the four reading datums encode the paper's central paired/nonpaired contrast — CWH bans paired, CS allows both.

def CitkoGracaninYuksek2025.cs_basic_sluice_what : Phenomena.Ellipsis.Sluicing.SluicingDatum

The "what" conjunct of cs_basic as a standalone sluice: "John taught something, but I forgot what."

Equations

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

def CitkoGracaninYuksek2025.cs_basic_sluice_when : Phenomena.Ellipsis.Sluicing.SluicingDatum

The "when" conjunct of cs_basic as a standalone sluice: "John taught (then), but I forgot when."

Equations

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

theorem CitkoGracaninYuksek2025.cs_basic_decomposes_into_sluices : cs_basic.whPhrases = [cs_basic_sluice_what.whPhrase, cs_basic_sluice_when.whPhrase]

Each CS decomposes into sluices: the wh-phrases in a CS are each sluice remnants.

theorem CitkoGracaninYuksek2025.cs_components_grammatical : cs_basic_sluice_what.grammatical = true ∧ cs_basic_sluice_when.grammatical = true

Both component sluices are grammatical.

def CitkoGracaninYuksek2025.cs_oblig_sluice_what : Phenomena.Ellipsis.Sluicing.SluicingDatum

The "what" and "to whom" conjuncts of cs_obligatory_args_allowed.

Equations

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

def CitkoGracaninYuksek2025.cs_oblig_sluice_toWhom : Phenomena.Ellipsis.Sluicing.SluicingDatum

Equations

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

theorem CitkoGracaninYuksek2025.cs_obligatory_decomposes : cs_obligatory_args_allowed.whPhrases = [cs_oblig_sluice_what.whPhrase, cs_oblig_sluice_toWhom.whPhrase]

Obligatory-argument CS also decomposes into sluices.

Bulgarian, German, Greek MWF data live in Phenomena/Questions/MultipleWh.lean (textbook-consensus typology). The intra-English variety A/B split is paper-specific to @cite{citko-gracanin-yuksek-2025} (p. 19): both varieties are non-MWF in matrix questions, but they diverge on multiple sluicing — variety A bans it, variety B allows it. The paper derives this asymmetry from where the PF asterisk lands (vP only vs both vP and CP edges), not as a free parameter. The tri-valued MWFParameter in MultipleWh.lean captures this derivation: variety B is .nonFrontsVPOnly, variety A is .nonFrontsBothEdges.

def CitkoGracaninYuksek2025.english : Typology.Question.MWFParameter

English (default): variety A — both vP and CP asterisks; no sluicing repair.

Equations

• CitkoGracaninYuksek2025.english = Typology.Question.MWFParameter.nonFrontsBothEdges

theorem CitkoGracaninYuksek2025.english_bans_multiple_wh : Typology.Question.MWFViolation english 2

English bans multiple wh-specifiers at a phase edge.

theorem CitkoGracaninYuksek2025.english_allows_single_wh : ¬Typology.Question.MWFViolation english 1

A single wh-specifier is fine in English.

def CitkoGracaninYuksek2025.english_varietyA : Phenomena.Questions.MultipleWh.MWFLanguageDatum

English variety A: non-MWF, bans multiple sluicing. The CP-edge asterisk survives ellipsis (vP-edge deletion is not enough).

Equations

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

def CitkoGracaninYuksek2025.english_varietyB : Phenomena.Questions.MultipleWh.MWFLanguageDatum

English variety B: non-MWF, allows multiple sluicing. Only the vP edge has the asterisk; vP-edge deletion repairs it.

Equations

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

theorem CitkoGracaninYuksek2025.english_variety_split : ¬english_varietyA.AllowsMultipleSluicing ∧ english_varietyB.AllowsMultipleSluicing

Variety A bans multiple sluicing, variety B allows it. Derived from the parameter via EllipsisRepairsMWF, not stipulated as an independent Bool.

Cost defs unchanged in shape from earlier revisions. The 4-Nat parameterization (sm/sl/nsm/nsl coarse, hm/hl/pm/pl/wm/wl fine) is ergonomically cryptic but matches the paper's argument granularity:

Coarse (MD vs ellipsis): parameterized by total shared/non-shared cost. Used for Theorems 1–2.

• sm/sl: Merge/lexical cost of shared material (built once with MD, twice with ellipsis)
• nsm/nsl: cost of non-shared parts (wh-movement, coordination)

Fine (non-bulk vs bulk sharing): decomposes shared material into heads vs phrasal structure. Used for Theorem 3.

• hm/hl: cost of shared heads (C, T — built once either way)
• pm/pl: cost of per-conjunct phrasal structure (C', TP, vP assembly)
• wm/wl: cost of wh-phrases + coordination (non-shared)

def CitkoGracaninYuksek2025.cwhMDCost (sm sl nsm nsl : ℕ) : Minimalist.DerivationCost

Cost of CWH via non-bulk-sharing MD (adopted structure, paper's (10b)). Shared material built once; no ellipsis.

Equations

• CitkoGracaninYuksek2025.cwhMDCost sm sl nsm nsl = { lexicalItems := sl + nsl, mergeOps := sm + nsm, agreeOps := 0, ellipsisOps := 0 }

def CitkoGracaninYuksek2025.cwhEllipsisCost (sm sl nsm nsl : ℕ) : Minimalist.DerivationCost

Cost of CWH via ellipsis (biclausal alternative, paper's (11b)). Shared material duplicated; one E-feature deletion.

Equations

• CitkoGracaninYuksek2025.cwhEllipsisCost sm sl nsm nsl = { lexicalItems := 2 * sl + nsl, mergeOps := 2 * sm + nsm, agreeOps := 0, ellipsisOps := 1 }

def CitkoGracaninYuksek2025.cwhNonBulkCost (hm hl pm pl wm wl : ℕ) : Minimalist.DerivationCost

Cost of CWH via non-bulk-sharing MD — fine-grained (paper's (10b)). Individual heads (C, T) shared; per-conjunct phrasal structure (assembling C', TP, vP around shared heads) built in each conjunct.

Equations

• CitkoGracaninYuksek2025.cwhNonBulkCost hm hl pm pl wm wl = { lexicalItems := hl + 2 * pl + wl, mergeOps := hm + 2 * pm + wm, agreeOps := 0, ellipsisOps := 0 }

def CitkoGracaninYuksek2025.cwhBulkMDCost (hm hl pm pl wm wl : ℕ) : Minimalist.DerivationCost

Cost of CWH via bulk-sharing MD (excluded, paper's (12b)). Entire C' shared — phrasal structure built only once. More economical than non-bulk-sharing, but blocked by MWF.

Equations

• CitkoGracaninYuksek2025.cwhBulkMDCost hm hl pm pl wm wl = { lexicalItems := hl + pl + wl, mergeOps := hm + pm + wm, agreeOps := 0, ellipsisOps := 0 }

def CitkoGracaninYuksek2025.csBulkCost (sm sl nsm nsl : ℕ) : Minimalist.DerivationCost

Cost of CS via bulk-sharing MD + single ellipsis (adopted, paper's (20b)). C' shared; E-feature on C deletes TP once.

Equations

• CitkoGracaninYuksek2025.csBulkCost sm sl nsm nsl = { lexicalItems := sl + nsl, mergeOps := sm + nsm, agreeOps := 0, ellipsisOps := 1 }

def CitkoGracaninYuksek2025.csDoubleEllipsisCost (sm sl nsm nsl : ℕ) : Minimalist.DerivationCost

Cost of CS via double ellipsis, no MD (excluded, paper's (19b)). Both conjuncts built in full; E-feature in each.

Equations

• CitkoGracaninYuksek2025.csDoubleEllipsisCost sm sl nsm nsl = { lexicalItems := 2 * sl + nsl, mergeOps := 2 * sm + nsm, agreeOps := 0, ellipsisOps := 2 }

theorem CitkoGracaninYuksek2025.cwh_md_beats_ellipsis (sm sl nsm nsl : ℕ) : Minimalist.strictlyMoreEconomical (cwhMDCost sm sl nsm nsl) (cwhEllipsisCost sm sl nsm nsl)

Theorem 1: For CWHs, the MD derivation is strictly more economical than the ellipsis alternative (paper's (10b) vs (11b)).

The MD derivation saves sm Merge ops and sl lexical items, and avoids the ellipsis op entirely. This holds for ANY shared material — even sm = sl = 0, the ellipsis op alone makes the alternative costlier.

theorem CitkoGracaninYuksek2025.cs_bulk_beats_double_ellipsis (sm sl nsm nsl : ℕ) : Minimalist.strictlyMoreEconomical (csBulkCost sm sl nsm nsl) (csDoubleEllipsisCost sm sl nsm nsl)

Theorem 2: For CSs, the bulk-sharing derivation is strictly more economical than the double-ellipsis alternative (paper's (20b) vs (19b)).

The bulk-sharing derivation saves sm Merge operations and sl lexical items, and uses one fewer ellipsis operation.

theorem CitkoGracaninYuksek2025.cwh_bulk_beats_nonbulk (hm hl pm pl wm wl : ℕ) (h : 0 < pm ∨ 0 < pl) : Minimalist.strictlyMoreEconomical (cwhBulkMDCost hm hl pm pl wm wl) (cwhNonBulkCost hm hl pm pl wm wl)

Theorem 3: Bulk-sharing is strictly more economical than non-bulk-sharing for CWHs (paper's (12b) vs (10b)).

The paper's crucial insight: the MOST economical derivation for CWHs (bulk-sharing, which builds C' once) is blocked by an independent constraint (MWF), forcing the LESS economical non-bulk-sharing structure. The precondition 0 < pm ∨ 0 < pl ensures there is at least some phrasal structure to share — which holds for any non-trivial clause.

Identifying economy winners

The Theorems 1-3 above establish strict-domination facts; combining each with Minimalist.economy_winner_of_pair (which discharges the existence guarantee from economy_admits_winner for the binary case) identifies the actual economy winner of the relevant 2-candidate reference set. These are the load-bearing wirings: C&G-Y's selection arguments need both "X dominates Y" AND "the reference set has a winner" to deliver "X is THE winner".

theorem CitkoGracaninYuksek2025.cwh_md_is_economy_winner (sm sl nsm nsl : ℕ) (alt : Minimalist.DerivationCost) : alt ∈ {cwhMDCost sm sl nsm nsl, cwhEllipsisCost sm sl nsm nsl} → ¬Minimalist.strictlyMoreEconomical alt (cwhMDCost sm sl nsm nsl)

CWH economy winner: of the reference set {cwhMDCost, cwhEllipsisCost}, cwhMDCost is an economy winner — no element of the set is strictly more economical than it. Wires cwh_md_beats_ellipsis through Minimalist.economy_winner_of_pair.

theorem CitkoGracaninYuksek2025.cs_bulk_is_economy_winner (sm sl nsm nsl : ℕ) (alt : Minimalist.DerivationCost) : alt ∈ {csBulkCost sm sl nsm nsl, csDoubleEllipsisCost sm sl nsm nsl} → ¬Minimalist.strictlyMoreEconomical alt (csBulkCost sm sl nsm nsl)

CS economy winner: of the reference set {csBulkCost, csDoubleEllipsisCost}, csBulkCost is an economy winner. Wires cs_bulk_beats_double_ellipsis through Minimalist.economy_winner_of_pair.

The CS (bulk-sharing) structure places both wh-phrases inside a single vP. Both must pass through the vP phase edge, creating a phase node with multiple wh-specifiers (paper's (36b)/(37b)).

In a non-MWF language like English, this configuration receives an asterisk at PF, crashing the derivation.

Unlike CSs, CWHs do NOT involve ellipsis — the vP edge survives to PF, so the asterisk is not deleted and the crash is unavoidable.

CSs survive because the E-feature on C triggers TP deletion (including the offending vP edge), removing the asterisk before PF interprets it.

theorem CitkoGracaninYuksek2025.cwh_bulk_crashes_in_english : Typology.Question.MWFViolation english 2

The bulk-sharing structure for CWHs crashes in English: 2 wh-specifiers at vP edge in a non-MWF language.

theorem CitkoGracaninYuksek2025.cwh_no_ellipsis_repair : ¬Typology.Question.EllipsisRepairsMWF english 2 false

CWHs have no ellipsis to repair the MWF violation — the vP edge survives to PF, and the asterisk crashes.

theorem CitkoGracaninYuksek2025.cs_ellipsis_repairs_mwf_varietyB : Typology.Question.EllipsisRepairsMWF english_varietyB.mwfParam 2 true

In English variety B (vP-only asterisk), CSs survive the same MWF configuration because ellipsis deletes the vP edge. Variety A (both-edges asterisk) is not repairable — CP-edge survives.

Paper p. 32 (re. ex (45c)): "If both Cs had the E feature, … Pronunciation Economy would be violated since the TP would be elided twice (once by the E feature on each C)."

The argument depends on the CS structure where a shared TP has two Cs each bearing the E-feature. Both Cs fire the E-feature on the same TP — but only the first deletion has any PF effect; the second targets material the first already removed. This is the per-operation vacuity that requires the new pronunciationEconomy : List PFOperation → Prop shape: a whole-derivation pfBefore ≠ pfAfter check would let this through (the first deletion ensures the whole derivation's PF differs).

def CitkoGracaninYuksek2025.cs_twoEFeature_initialPF : List String

Initial PF state of the shared TP: contains "John taught".

Equations

• CitkoGracaninYuksek2025.cs_twoEFeature_initialPF = ["John", "taught"]

def CitkoGracaninYuksek2025.cs_twoEFeature_firstDeletion : Minimalist.PFOperation

The first C's E-feature deletion: removes "John taught" from the shared TP. Non-vacuous.

Equations

• CitkoGracaninYuksek2025.cs_twoEFeature_firstDeletion = { pfBefore := CitkoGracaninYuksek2025.cs_twoEFeature_initialPF, pfAfter := [] }

def CitkoGracaninYuksek2025.cs_twoEFeature_secondDeletion : Minimalist.PFOperation

The second C's E-feature deletion: tries to delete the same shared TP, but it is already empty after the first deletion. Vacuous.

Equations

• CitkoGracaninYuksek2025.cs_twoEFeature_secondDeletion = { pfBefore := [], pfAfter := [] }

def CitkoGracaninYuksek2025.cs_twoEFeature_deletions : List Minimalist.PFOperation

The full deletion sequence under a hypothetical two-E-feature CS structure (paper's (45c) configuration).

Equations

• CitkoGracaninYuksek2025.cs_twoEFeature_deletions = [CitkoGracaninYuksek2025.cs_twoEFeature_firstDeletion, CitkoGracaninYuksek2025.cs_twoEFeature_secondDeletion]

theorem CitkoGracaninYuksek2025.cs_twoEFeature_secondDeletion_vacuous : cs_twoEFeature_secondDeletion.isVacuous

The second deletion is vacuous (its PF before/after coincide).

theorem CitkoGracaninYuksek2025.cs_twoEFeature_violates_pronunciation_economy : ¬Minimalist.pronunciationEconomy cs_twoEFeature_deletions

The two-E-feature CS structure violates Pronunciation Economy at the second deletion. This is the paper's (45c) ban — the per-op vacuity is what rules it out, even though the full derivation's pfBefore (["John", "taught"]) ≠ pfAfter ([]) is satisfied.

A whole-derivation PF≠ check would pass this configuration incorrectly; the per-op pronunciationEconomy correctly fails it.

theorem CitkoGracaninYuksek2025.cs_twoEFeature_wholeDeriv_pf_differs : cs_twoEFeature_initialPF ≠ []

Whole-derivation PF differs (initial ["John","taught"] → final []) even though the second op is vacuous. This is exactly what makes a whole-derivation PF≠ check inadequate for the paper's argument.

def CitkoGracaninYuksek2025.cwhStructure : Minimalist.PFReducedCoordination

The adopted CWH structure: non-bulk-sharing MD, no ellipsis (paper's (10b)). Shared nodes: C and T are individually multiply dominated.

Equations

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

def CitkoGracaninYuksek2025.csStructure : Minimalist.PFReducedCoordination

The adopted CS structure: bulk-sharing MD + ellipsis (paper's (20b)). The E-feature on C (cf. FeatureVal.ellipsis in Core/Features.lean) triggers TP deletion, repairing the MWF violation at the vP edge. Shared nodes: entire C' is shared (includes C, TP, vP, VP).

Equations

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

theorem CitkoGracaninYuksek2025.cwhStructure_csStructure_drift_sentry : cwhStructure.UsesMD ∧ ¬cwhStructure.UsesEllipsis ∧ csStructure.UsesBoth ∧ cwhStructure.sharedNodes.length = 2 ∧ csStructure.sharedNodes.length = 3 ∧ (cwhStructure.sharedNodes.all fun (x : Minimalist.SharedNode) => x.category.isSome) = true ∧ (csStructure.sharedNodes.all fun (x : Minimalist.SharedNode) => x.category.isSome) = true

Structural drift sentry over the four key properties of cwhStructure and csStructure. Replaces five individual rfl theorems (cwh_uses_md_only, cs_uses_both, cwh_shares_heads_cs_shares_constituent, cwh_shared_categories, cs_shared_categories).

The paper's central contribution is explaining WHY CWHs and CSs must have different structures — and therefore different empirical properties — despite their superficial similarity.

For CWHs (§4.1):

1. Bulk-sharing MD is most economical (cwh_bulk_beats_nonbulk)
2. But bulk-sharing creates MWF violation at vP (cwh_bulk_crashes_in_english)
3. CWHs have no ellipsis to repair MWF (cwh_no_ellipsis_repair)
4. So non-bulk-sharing MD is selected (cwh_md_beats_ellipsis over ellipsis)

For CSs (§4.2):

1. Bulk-sharing MD + ellipsis is most economical (cs_bulk_beats_double_ellipsis)
2. Bulk-sharing creates MWF at vP, but ellipsis repairs it (cs_ellipsis_repairs_mwf_varietyB, in vP-only varieties)
3. Non-bulk-sharing (CWH structure) violates Pronunciation Economy (cs_twoEFeature_violates_pronunciation_economy)
4. So bulk-sharing MD + ellipsis is selected

theorem CitkoGracaninYuksek2025.different_mechanisms : cwhStructure.mechanisms ≠ csStructure.mechanisms

The two constructions differ in which mechanisms they use.

theorem CitkoGracaninYuksek2025.different_sharing : cwhStructure.sharing ≠ csStructure.sharing

The two constructions differ in sharing type.

theorem CitkoGracaninYuksek2025.cwh_forced_to_nonbulk (hm hl pm pl wm wl : ℕ) (h : 0 < pm ∨ 0 < pl) : Minimalist.strictlyMoreEconomical (cwhBulkMDCost hm hl pm pl wm wl) (cwhNonBulkCost hm hl pm pl wm wl) ∧ Typology.Question.MWFViolation english 2 ∧ ¬Typology.Question.EllipsisRepairsMWF english 2 false

End-to-end: CWHs cannot use bulk-sharing (most economical) because the MWF violation at vP cannot be repaired without ellipsis. Combines Theorem 3, cwh_bulk_crashes_in_english, and cwh_no_ellipsis_repair.

theorem CitkoGracaninYuksek2025.cs_forced_to_bulk (sm sl nsm nsl : ℕ) : Minimalist.strictlyMoreEconomical (csBulkCost sm sl nsm nsl) (csDoubleEllipsisCost sm sl nsm nsl) ∧ Typology.Question.EllipsisRepairsMWF english_varietyB.mwfParam 2 true ∧ ¬Minimalist.pronunciationEconomy cs_twoEFeature_deletions

End-to-end: CSs use bulk-sharing because it is most economical AND the MWF violation is repaired by ellipsis (in vP-only varieties); the CWH (two-E-feature) structure is excluded by per-op Pronunciation Economy.

Section 6.2 of the paper extends the economy analysis to Right Node Raising (RNR). RNR is a key test case because it can involve BOTH ellipsis and MD simultaneously — the "mix and match" analysis of @cite{belk-neeleman-philip-2023} (and earlier @cite{barros-vicente-2011}).

The core claim: economy favors MD over ellipsis when both yield the same string and interpretation. In RNR, the shared pivot (rightmost material) is multiply dominated. When the pivot and antecedent are not morphologically identical (vehicle change), ellipsis is additionally required for the non-shared material in the first conjunct.

inductive CitkoGracaninYuksek2025.RNRPivotType : Type

RNR pivot type: what is shared at the right edge.

• minimal : RNRPivotType

  Only the rightmost constituent (e.g., PP) is shared.

• extended : RNRPivotType

  A larger constituent (e.g., VP) is shared.

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprRNRPivotType : Repr RNRPivotType

Equations

• CitkoGracaninYuksek2025.instReprRNRPivotType = { reprPrec := CitkoGracaninYuksek2025.instReprRNRPivotType.repr }

def CitkoGracaninYuksek2025.instReprRNRPivotType.repr : RNRPivotType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqRNRPivotType : DecidableEq RNRPivotType

Equations

• CitkoGracaninYuksek2025.instDecidableEqRNRPivotType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CitkoGracaninYuksek2025.RNRDatum : Type

An RNR datum captures the structural analysis.

• sentence : String
• pivot : String

  The shared pivot string (right-edge material).

• morphologicalIdentity : Bool

  Does the pivot exhibit morphological identity with the antecedent?

• mdProperties : Bool

  Does the pivot exhibit properties of MD? (e.g., cumulative agreement, internal reading of relational adjective)

• involvesEllipsis : Bool

  Does the construction involve ellipsis in addition to MD?

• pivotType : RNRPivotType
• notes : String

def CitkoGracaninYuksek2025.instReprRNRDatum.repr : RNRDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprRNRDatum : Repr RNRDatum

Equations

• CitkoGracaninYuksek2025.instReprRNRDatum = { reprPrec := CitkoGracaninYuksek2025.instReprRNRDatum.repr }

def CitkoGracaninYuksek2025.rnr_pureMD : RNRDatum

Pure MD: identical verbs, no mismatch → economy selects MD only (ex 55).

Equations

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

def CitkoGracaninYuksek2025.rnr_ellipsisPlusMD : RNRDatum

Ellipsis + MD: verb morphology mismatch forces ellipsis for VP, but PP pivot is still shared via MD (ex 52/53).

Equations

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

def CitkoGracaninYuksek2025.rnr_ellipsisOnly : RNRDatum

Vehicle-change diagnostic from @cite{barros-vicente-2011} ex (47): morphological mismatch signals ellipsis (not MD).

The angled brackets mark the first conjunct's predicate as PF-reduced under identity with the second conjunct's overt predicate — backwards elision, not forwards RNR with a right-edge pivot. The morphological mismatch (wake vs wakes) confirms ellipsis (which tolerates vehicle change) over MD (which requires morphological identity for a single multiply-dominated node).

Equations

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

def CitkoGracaninYuksek2025.rnr_internalReading : RNRDatum

Relational adjective with internal reading signals MD.

Equations

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

theorem CitkoGracaninYuksek2025.rnr_typology_drift_sentry : rnr_pureMD.morphologicalIdentity = true ∧ rnr_pureMD.mdProperties = true ∧ rnr_pureMD.involvesEllipsis = false ∧ rnr_ellipsisPlusMD.morphologicalIdentity = false ∧ rnr_ellipsisPlusMD.mdProperties = true ∧ rnr_ellipsisPlusMD.involvesEllipsis = true ∧ rnr_internalReading.mdProperties = true ∧ rnr_internalReading.involvesEllipsis = false

RNR datum drift sentry: morphological-identity / MD-properties / ellipsis-involvement consistent with the paper's typology. Replaces rnr_economy_prefers_md and rnr_mismatch_forces_ellipsis.

def CitkoGracaninYuksek2025.rnrMDPivotCost (pivotMerge pivotLex nonsharedMerge nonsharedLex : ℕ) : Minimalist.DerivationCost

RNR pivot cost: MD derivation for the shared pivot. The pivot is built once (MD) rather than twice (ellipsis).

Equations

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

def CitkoGracaninYuksek2025.rnrEllipsisCost (pivotMerge pivotLex nonsharedMerge nonsharedLex : ℕ) : Minimalist.DerivationCost

RNR cost with full ellipsis (no MD): pivot duplicated.

Equations

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

theorem CitkoGracaninYuksek2025.rnr_md_beats_ellipsis (pm pl nm nl : ℕ) : Minimalist.strictlyMoreEconomical (rnrMDPivotCost pm pl nm nl) (rnrEllipsisCost pm pl nm nl)

Theorem 4: For RNR, MD is strictly more economical than ellipsis when both yield the same string. Same shape as Theorem 1.

theorem CitkoGracaninYuksek2025.rnr_md_is_economy_winner (pm pl nm nl : ℕ) (alt : Minimalist.DerivationCost) : alt ∈ {rnrMDPivotCost pm pl nm nl, rnrEllipsisCost pm pl nm nl} → ¬Minimalist.strictlyMoreEconomical alt (rnrMDPivotCost pm pl nm nl)

RNR economy winner: of the reference set {rnrMDPivotCost, rnrEllipsisCost}, rnrMDPivotCost is an economy winner. Wires rnr_md_beats_ellipsis through Minimalist.economy_winner_of_pair.

@cite{bruening-2021}'s max-projection identity condition for ellipsis (formalized as Minimalist.Ellipsis.FormalMatching.bruening2021StructurallyIdentical) requires the antecedent and the elided constituent to have the same filtered max-projection path lists (up to permutation).

In the C&G-Y CS bulk-sharing structure, the elided TP literally is the antecedent TP — one node in the multidominance graph with two parents. So the filtered max-projection paths are physically identical, and List.Perm.refl discharges the identity condition.

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

The C&G-Y CS bulk-sharing structure is robust to identity-condition choice: it trivially satisfies @cite{bruening-2021}'s max-projection identity by List.Perm.refl on identical path lists, for any HeadFunction parameterizing the projection paths.

This is a positive cross-framework consilience: the C&G-Y MD architecture and the Bruening 2021 identity condition agree on CS, so the paper's predictions for CS sluicing licensing do not depend on identity-condition choice.