Economy in PF Reduction

[CGY25]

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 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) and the intra-English variety A/B split — paper-specific to [CGY25] — live in §2 over that substrate.
• Pronunciation Economy is the per-operation primitive pronunciationEconomy : List PFOperation → Prop from 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.

Integration

• CSs are coordinated sluices — each conjunct of a CS is a sluice. §1b decomposes CS examples into standalone component sluices.
• The MWF parameter (Typology/Question.lean) classifies languages: 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 ([BNP23], [BV11]).

Multidominance (relocated from Minimalist/Multidominance.lean)

A multidominance (MD) structure is a syntactic object built once that is structurally accessible from two (or more) dominating nodes. At PF, it linearizes once. MD is one of the two main mechanisms for producing PF-reduced representations (representations where some material is interpreted but not pronounced); the other is ellipsis. [Cit14] [Wil08a]

The MD primitives any MD-using analysis needs:

• PFReductionMechanism — the two PF-reduction mechanisms (ellipsis vs multidominance);
• MDSharing — bulk vs non-bulk sharing in coordination;
• SharedNode — a multiply-dominated node + its category + whether it is pronounced;
• PFReducedCoordination — a coordinate &P with PF reduction.

Anchored on [Cit14] (textbook treatment of parallel-Merge MD) and [Wil08a] (constituent-sharing flavor).

Convention notes

• This does not commit to a particular MD flavor (parallel-Merge vs constituent-sharing vs 3-D phrase structure). SharedNode records the multiply-dominated node abstractly; specific MD theories instantiate the dominance/sharing relation via their own apparatus.
• MDSharing was renamed from SharingType at 0.230.575 to avoid a bare-name collision with Syntax/DependencyGrammar/Formal/CoordinationParallelism.lean's SharingType (which classifies extraction symmetry, not constituent sharing).
• UsesMD / UsesEllipsis / UsesBoth are Prop with decidability instances (per feedback_no_intrinsic_bool discipline); decide-checked consumers continue to work.

inductive CitkoGracaninYuksek2025.PFReductionMechanism : Type

The two mechanisms of PF reduction.

Both produce representations where material is interpreted but not pronounced. Economy (Syntax/Minimalist/Economy.lean) governs the choice between them.

• ellipsis : PFReductionMechanism

  E-feature on a functional head triggers deletion of its complement at PF. The deleted material is built in full during the derivation.

• multidominance : PFReductionMechanism

  A syntactic object is built once and shared between two dominating nodes. Pronounced at one position only.

def CitkoGracaninYuksek2025.instReprPFReductionMechanism.repr : PFReductionMechanism → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprPFReductionMechanism : Repr PFReductionMechanism

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqPFReductionMechanism : DecidableEq PFReductionMechanism

Equations

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

inductive CitkoGracaninYuksek2025.MDSharing : Type

How material is shared between conjuncts in an MD coordination.

The empirical motivation is [CGY25]: coordinated wh-questions use non-bulk-sharing (individual heads shared), while coordinated sluices use bulk-sharing (entire C' shared). The two sharing modes derive different syntactic and interpretive properties.

NB: name distinguished from Syntax/DependencyGrammar/Formal/CoordinationParallelism.SharingType (extraction symmetry, not constituent sharing).

• nonBulk : MDSharing

  Individual functional heads shared between conjuncts. Each conjunct remains a separate full phrase; only specific heads (e.g., C, T) are multiply dominated.

• bulk : MDSharing

  An entire constituent is shared between conjuncts. Both conjuncts dominate the same subtree, so they share all material inside it (C, TP, vP, VP, ...).

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprMDSharing : Repr MDSharing

Equations

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

def CitkoGracaninYuksek2025.instReprMDSharing.repr : MDSharing → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqMDSharing : DecidableEq MDSharing

Equations

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

structure CitkoGracaninYuksek2025.SharedNode : Type

A node shared between two conjuncts in a coordination structure.

The shared node is built once but is structurally accessible from both parent1 and parent2. At PF, it is linearized once.

• node : Minimalist.SyntacticObject

  The multiply dominated node.

• category : Option Minimalist.Cat

  Category of the shared node, when labelled.

• pronounced : Bool

  The shared node has PF content (vs. is silent).

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprSharedNode : Repr SharedNode

Equations

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

def CitkoGracaninYuksek2025.instReprSharedNode.repr : SharedNode → ℕ → Std.Format

Equations

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

def CitkoGracaninYuksek2025.instDecidableEqSharedNode.decEq (x✝ x✝¹ : SharedNode) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqSharedNode : DecidableEq SharedNode

Equations

• CitkoGracaninYuksek2025.instDecidableEqSharedNode = CitkoGracaninYuksek2025.instDecidableEqSharedNode.decEq

structure CitkoGracaninYuksek2025.PFReducedCoordination : Type

A coordination structure with PF reduction.

Models a coordinate &P where material is either multiply dominated (shared between conjuncts) or elided by an E-feature.

Substrate note (post-MCB Phase 1.0). The conjunct1 / conjunct2 field names are stipulated planar labels at the coord-structure meta-level, NOT inherited from the SO substrate (which is nonplanar via FreeCommMagma — see Minimalist.merge_comm). The first-vs-second conjunct distinction tracked by these fields is a coordination- specific stipulation about which conjunct hosts the shared / deleted material, parallel to BrueningAlKhalaf2020.mergeCoordSymmetry. Phase 2+: harmonize with [Cit11]'s symmetric-merge multidominance framework, where conjunct ordering is genuinely a multiset operation.

• conjunct1 : Minimalist.SyntacticObject

  First conjunct. Planar label is stipulated at coord-structure level (not inherited from substrate).

• conjunct2 : Minimalist.SyntacticObject

  Second conjunct.

• mechanisms : List PFReductionMechanism

  PF reduction mechanism(s) used.

• sharing : Option MDSharing

  Mode of sharing (for MD structures).

• sharedNodes : List SharedNode

  Nodes that are shared or deleted.

• pfOutput : List String

  PF output after reduction.

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprPFReducedCoordination : Repr PFReducedCoordination

Equations

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

def CitkoGracaninYuksek2025.instReprPFReducedCoordination.repr : PFReducedCoordination → ℕ → Std.Format

Equations

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

def CitkoGracaninYuksek2025.instDecidableEqPFReducedCoordination.decEq (x✝ x✝¹ : PFReducedCoordination) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqPFReducedCoordination : DecidableEq PFReducedCoordination

Equations

• CitkoGracaninYuksek2025.instDecidableEqPFReducedCoordination = CitkoGracaninYuksek2025.instDecidableEqPFReducedCoordination.decEq

def CitkoGracaninYuksek2025.PFReducedCoordination.UsesMD (c : PFReducedCoordination) : Prop

Does this coordination use multidominance?

Equations

• c.UsesMD = (CitkoGracaninYuksek2025.PFReductionMechanism.multidominance ∈ c.mechanisms)

@[implicit_reducible]

instance CitkoGracaninYuksek2025.PFReducedCoordination.instDecidableUsesMD (c : PFReducedCoordination) : Decidable c.UsesMD

Equations

• c.instDecidableUsesMD = id inferInstance

def CitkoGracaninYuksek2025.PFReducedCoordination.UsesEllipsis (c : PFReducedCoordination) : Prop

Does this coordination use ellipsis?

Equations

• c.UsesEllipsis = (CitkoGracaninYuksek2025.PFReductionMechanism.ellipsis ∈ c.mechanisms)

@[implicit_reducible]

instance CitkoGracaninYuksek2025.PFReducedCoordination.instDecidableUsesEllipsis (c : PFReducedCoordination) : Decidable c.UsesEllipsis

Equations

• c.instDecidableUsesEllipsis = id inferInstance

def CitkoGracaninYuksek2025.PFReducedCoordination.UsesBoth (c : PFReducedCoordination) : Prop

Does this coordination use both MD and ellipsis?

Equations

• c.UsesBoth = (c.UsesMD ∧ c.UsesEllipsis)

@[implicit_reducible]

instance CitkoGracaninYuksek2025.PFReducedCoordination.instDecidableUsesBoth (c : PFReducedCoordination) : Decidable c.UsesBoth

Equations

• c.instDecidableUsesBoth = id inferInstance

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."

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

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprWHCoordType : Repr WHCoordType

Equations

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

@[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).

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprReadingType : Repr ReadingType

Equations

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

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

Equations

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

@[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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprReadingDatum : Repr ReadingDatum

Equations

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

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

Equations

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

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.

structure CitkoGracaninYuksek2025.ComponentSluice : Type

One conjunct of a coordinated sluice, recast as a standalone sluice.

• sentence : String
• whPhrase : String
• grammatical : Bool

def CitkoGracaninYuksek2025.instReprComponentSluice.repr : ComponentSluice → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprComponentSluice : Repr ComponentSluice

Equations

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

def CitkoGracaninYuksek2025.instDecidableEqComponentSluice.decEq (x✝ x✝¹ : ComponentSluice) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqComponentSluice : DecidableEq ComponentSluice

Equations

• CitkoGracaninYuksek2025.instDecidableEqComponentSluice = CitkoGracaninYuksek2025.instDecidableEqComponentSluice.decEq

def CitkoGracaninYuksek2025.cs_basic_sluice_what : ComponentSluice

The "what" conjunct of cs_basic as a standalone sluice (antecedent "John taught something", correlate "something", elided "John taught").

Equations

• CitkoGracaninYuksek2025.cs_basic_sluice_what = { sentence := "John taught something, but I forgot what.", whPhrase := "what" }

def CitkoGracaninYuksek2025.cs_basic_sluice_when : ComponentSluice

The "when" conjunct of cs_basic as a standalone sluice (antecedent "John taught (then)", correlate "(then)", elided "John taught").

Equations

• CitkoGracaninYuksek2025.cs_basic_sluice_when = { sentence := "John taught (then), but I forgot when.", whPhrase := "when" }

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 : ComponentSluice

The "what" conjunct of cs_obligatory_args_allowed (correlate "something", elided "John gave (to someone)").

Equations

• CitkoGracaninYuksek2025.cs_oblig_sluice_what = { sentence := "John gave something to someone, but I forgot what.", whPhrase := "what" }

def CitkoGracaninYuksek2025.cs_oblig_sluice_toWhom : ComponentSluice

The "to whom" conjunct of cs_obligatory_args_allowed (correlate "to someone", elided "John gave (something)").

Equations

• CitkoGracaninYuksek2025.cs_oblig_sluice_toWhom = { sentence := "John gave something to someone, but I forgot to whom.", whPhrase := "to whom" }

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.

Languages vary in whether multiple wh-specifiers at a phase edge are tolerable at PF ([Rud88], [CGY25]). The substrate primitives (MWFParameter, PhaseEdge, EdgeAsterisk, MWFViolation, EllipsisRepairsMWF) are in Typology/Question.lean; this section holds the per-language data and theorems consuming them.

The intra-English variety A/B split is paper-specific to [CGY25] (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: variety B is .nonFrontsVPOnly, variety A is .nonFrontsBothEdges.

structure CitkoGracaninYuksek2025.MWFLanguageDatum : Type

Cross-linguistic MWF datum. Records the parameter setting and an example question. AllowsMultipleSluicing is derived from the parameter via EllipsisRepairsMWF.

• language : String
• mwfParam : Syntax.Question.MWFParameter
• exampleQuestion : String

  Example multiple wh-question.

• grammatical : Bool

  Is the bare multiple-wh question grammatical?

• notes : String

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instReprMWFLanguageDatum : Repr MWFLanguageDatum

Equations

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

def CitkoGracaninYuksek2025.instReprMWFLanguageDatum.repr : MWFLanguageDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqMWFLanguageDatum : DecidableEq MWFLanguageDatum

Equations

• CitkoGracaninYuksek2025.instDecidableEqMWFLanguageDatum = CitkoGracaninYuksek2025.instDecidableEqMWFLanguageDatum.decEq

def CitkoGracaninYuksek2025.instDecidableEqMWFLanguageDatum.decEq (x✝ x✝¹ : MWFLanguageDatum) : Decidable (x✝ = x✝¹)

Equations

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

def CitkoGracaninYuksek2025.MWFLanguageDatum.AllowsMultipleSluicing (d : MWFLanguageDatum) : Prop

Multiple sluicing is licensed iff vP-edge ellipsis repairs the MWF violation for n = 2 wh-specifiers. Derived, not stipulated.

Equations

• d.AllowsMultipleSluicing = Syntax.Question.EllipsisRepairsMWF d.mwfParam 2 true

@[implicit_reducible]

instance CitkoGracaninYuksek2025.instDecidableAllowsMultipleSluicing (d : MWFLanguageDatum) : Decidable d.AllowsMultipleSluicing

Equations

• CitkoGracaninYuksek2025.instDecidableAllowsMultipleSluicing d = id inferInstance

def CitkoGracaninYuksek2025.bulgarian : MWFLanguageDatum

Bulgarian: MWF language ([Rud88] canonical case).

Equations

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

def CitkoGracaninYuksek2025.german : MWFLanguageDatum

German: non-MWF; vP-only asterisk; multiple sluicing repairs. [CGY25] ex 31a.

Equations

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

def CitkoGracaninYuksek2025.greek : MWFLanguageDatum

Greek: non-MWF; vP-only asterisk; multiple sluicing repairs. [CGY25] ex 31b.

Equations

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

def CitkoGracaninYuksek2025.mwfLanguageTable : List MWFLanguageDatum

Cross-linguistic MWF table (textbook-consensus subset).

Equations

• CitkoGracaninYuksek2025.mwfLanguageTable = [CitkoGracaninYuksek2025.bulgarian, CitkoGracaninYuksek2025.german, CitkoGracaninYuksek2025.greek]

theorem CitkoGracaninYuksek2025.bulgarian_no_violation : ¬Syntax.Question.MWFViolation bulgarian.mwfParam 2

Bulgarian: MWF language → no violations on bare multiple wh.

theorem CitkoGracaninYuksek2025.german_violates_in_questions : Syntax.Question.MWFViolation german.mwfParam 2

German question with two wh-phrases is starred.

theorem CitkoGracaninYuksek2025.german_greek_sluicing_repairs : german.AllowsMultipleSluicing ∧ greek.AllowsMultipleSluicing

Sluicing repairs in German and Greek (vP-only asterisk eliminated).

def CitkoGracaninYuksek2025.english : Syntax.Question.MWFParameter

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

Equations

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

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

English bans multiple wh-specifiers at a phase edge.

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

A single wh-specifier is fine in English.

def CitkoGracaninYuksek2025.english_varietyA : 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 : 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 : Syntax.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 : ¬Syntax.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 : Syntax.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 : 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 : 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 : SharedNode) => x.category.isSome) = true ∧ (csStructure.sharedNodes.all fun (x : 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) ∧ Syntax.Question.MWFViolation english 2 ∧ ¬Syntax.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) ∧ Syntax.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 [BNP23] (and earlier [BV11]).

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 [BV11] 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.