Derivational Economy

@cite{chomsky-1991} @cite{chomsky-1995} @cite{boskovic-1997} @cite{collins-2001} @cite{citko-gracanin-yuksek-2025}

Economy compares competing derivations that converge on the same PF string and LF interpretation, selecting the one with fewest operations and lexical resources.

Two principles

• Least Effort: Pareto-minimize on lexical items / Merge ops / Agree ops / E-feature deletions. Drawn from @cite{chomsky-1991}, @cite{chomsky-1995}, @cite{boskovic-1997}; the global transderivational variant per @cite{citko-gracanin-yuksek-2025} fn 3. The local-economy alternative (@cite{collins-2001}) is not formalized.

• Pronunciation Economy (@cite{citko-gracanin-yuksek-2025} p. 27): no PF-affecting operation is vacuous. Checked per operation, not on whole-derivation PF before/after — see pronunciationEconomy's docstring for why a whole-derivation ≠ check under-rejects.

Headline (§3): well-foundedness via Dickson's lemma

instance : WellFoundedLT DerivationCost lifts Pi.wellFoundedLT on Fin 4 → Nat (= Dickson 1913 applied to Nat^n) through the order embedding DerivationCost.profileEmbedding. This is what makes "economy selects an optimum from the reference set" mathematically coherent: without WF, an infinite chain of ever-more-economical derivations could exist and "the economy winner" would be ill-defined. WF is a precondition for the linguistic content, not a corollary.

The load-bearing corollary economy_admits_winner says any non-empty R : Set DerivationCost admits a Pareto-minimum. Consumers identifying a specific winner of a binary reference set (the common C&G-Y pattern) use the economy_winner_of_pair helper.

Architectural realization

DerivationCost is a 4-Nat record. Its preorder is the pullback of Pi.preorder on Fin 4 → Nat through DerivationCost.profile, realized via Core.Order.FeaturePreorder.ofFeature. Same shape as Core/Constraint/Pareto.lean's paretoFeaturePreorder (used for OT/HG candidate comparison); the OT side wraps in ConstraintSystem with candidate set + decoder, but Minimalist economy needs neither, so we register Preorder DerivationCost directly. coarsen_via_monotone from Core/Order/FeaturePreorder.lean is then available for free.

Removed (for git history)

Pre-Phase principles (Procrastinate, Last Resort, Greed) and overtOps field were removed at 0.230.574 — Bool-identity wrappers and a cost field no producer populated. Future consumers wanting Phase-Theoretic analogues should formalize against actual Step/Phase infrastructure.

structure Minimalist.DerivationCost : Type

4-dimensional cost of a syntactic derivation, measured by operation and resource counts. The dimensions are exactly those @cite{citko-gracanin-yuksek-2025} (p. 3) compares when arguing multidominance is more economical than ellipsis: lexical items drawn from the numeration, Merge operations, Agree operations, and E-feature triggered PF deletions.

• lexicalItems : ℕ
• mergeOps : ℕ
• agreeOps : ℕ
• ellipsisOps : ℕ

def Minimalist.instReprDerivationCost.repr : DerivationCost → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprDerivationCost : Repr DerivationCost

Equations

• Minimalist.instReprDerivationCost = { reprPrec := Minimalist.instReprDerivationCost.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqDerivationCost : DecidableEq DerivationCost

Equations

• Minimalist.instDecidableEqDerivationCost = Minimalist.instDecidableEqDerivationCost.decEq

def Minimalist.instDecidableEqDerivationCost.decEq (x✝ x✝¹ : DerivationCost) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.DerivationCost.profile (c : DerivationCost) : Fin 4 → ℕ

The 4-vector projection: profile c i is the i-th cost dimension (0 = lexicalItems, 1 = mergeOps, 2 = agreeOps, 3 = ellipsisOps). Feature map for the Core.Order.FeaturePreorder instance.

Equations

• c.profile ⟨0, isLt⟩ = c.lexicalItems
• c.profile ⟨1, isLt⟩ = c.mergeOps
• c.profile ⟨2, isLt⟩ = c.agreeOps
• c.profile ⟨3, isLt⟩ = c.ellipsisOps

@[simp]

theorem Minimalist.DerivationCost.profile_zero (c : DerivationCost) : c.profile 0 = c.lexicalItems

@[simp]

theorem Minimalist.DerivationCost.profile_one (c : DerivationCost) : c.profile 1 = c.mergeOps

@[simp]

theorem Minimalist.DerivationCost.profile_two (c : DerivationCost) : c.profile 2 = c.agreeOps

@[simp]

theorem Minimalist.DerivationCost.profile_three (c : DerivationCost) : c.profile 3 = c.ellipsisOps

def Minimalist.DerivationCost.featurePreorder : Core.Order.FeaturePreorder DerivationCost (Fin 4 → ℕ)

Cost-comparison preorder via FeaturePreorder.ofFeature pullback through profile, with Pi.preorder (pointwise ≤) on the Fin 4 → Nat feature space.

See module docstring § "Architectural realization" for the parallel with Core/Constraint/Pareto.lean's paretoFeaturePreorder.

Equations

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

@[implicit_reducible]

instance Minimalist.DerivationCost.instPreorder : Preorder DerivationCost

Equations

• Minimalist.DerivationCost.instPreorder = Minimalist.DerivationCost.featurePreorder.toPreorder

def Minimalist.Derivation.cost (d : Derivation) : DerivationCost

Extract cost from a core Derivation (step-based model).

lexicalItems: each emL/emR/wlm step draws one lexical item from the numeration. (Wholesale Late Merger @cite{takahashi-hulsey-2009} introduces a restrictor — also a numeration draw.) mergeOps: total step count. agreeOps/ellipsisOps: not tracked by the step-based model.

Equations

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

def Minimalist.atLeastAsEconomical (c1 c2 : DerivationCost) : Prop

Componentwise Pareto: c1 is at-least-as-economical as c2 iff every cost dimension is no worse. Linguistic-named alias for the underlying Preorder.le from DerivationCost.featurePreorder.

NB: this is not a flat sum. Earlier revisions used totalOps := mergeOps + agreeOps + ellipsisOps followed by 2-tuple (totalOps, lexicalItems) comparison, which lets a derivation with agreeOps=0, mergeOps=100 "beat" one with agreeOps=10, mergeOps=50 purely on the sum (110 vs 60) — a comparison @cite{citko-gracanin-yuksek-2025} (p. 3) explicitly does not endorse: they argue MD is more economical than ellipsis on the each-dimension reading (fewer lexical items AND fewer Merge AND fewer Agree).

Equations

• Minimalist.atLeastAsEconomical c1 c2 = (c1.lexicalItems ≤ c2.lexicalItems ∧ c1.mergeOps ≤ c2.mergeOps ∧ c1.agreeOps ≤ c2.agreeOps ∧ c1.ellipsisOps ≤ c2.ellipsisOps)

@[implicit_reducible]

instance Minimalist.instDecidableAtLeastAsEconomical (c1 c2 : DerivationCost) : Decidable (atLeastAsEconomical c1 c2)

Equations

• Minimalist.instDecidableAtLeastAsEconomical c1 c2 = id inferInstance

def Minimalist.strictlyMoreEconomical (c1 c2 : DerivationCost) : Prop

Strict Pareto: at-least-as-economical AND strictly better on at least one dimension. Equivalent to < from the Preorder instance (cf. strictlyMoreEconomical_iff_lt), but not definitionally equal.

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableStrictlyMoreEconomical (c1 c2 : DerivationCost) : Decidable (strictlyMoreEconomical c1 c2)

Equations

• Minimalist.instDecidableStrictlyMoreEconomical c1 c2 = id inferInstance

@[simp]

theorem Minimalist.atLeastAsEconomical_iff_le (c1 c2 : DerivationCost) : atLeastAsEconomical c1 c2 ↔ c1 ≤ c2

The linguistic alias agrees with ≤ from the FeaturePreorder pullback componentwise. Tagged @[simp] so consumers can rewrite freely between the linguistic and order-theoretic forms.

theorem Minimalist.strictlyMoreEconomical_iff_lt (c1 c2 : DerivationCost) : strictlyMoreEconomical c1 c2 ↔ c1 < c2

Strict economy is the strict order of the Preorder instance: at-least-as-economical AND strictly better on at least one dimension iff c1 ≤ c2 ∧ ¬ c2 ≤ c1.

Well-Foundedness — the headline (Dickson's lemma)

theorem Minimalist.DerivationCost.profile_injective : Function.Injective profile

profile is injective: a derivation cost is determined by its 4 components. Foundational fact for the OrderEmbedding and PartialOrder instances below.

def Minimalist.DerivationCost.profileEmbedding : DerivationCost ↪o (Fin 4 → ℕ)

Order embedding of DerivationCost into the 4-vector Pareto preorder on Fin 4 → Nat. map_rel_iff' is Iff.rfl because the Preorder DerivationCost instance is featurePreorder.toPreorder = Preorder.lift profile (≤ is definitionally profile a ≤ profile b).

Equations

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

@[implicit_reducible]

instance Minimalist.instPartialOrderDerivationCost : PartialOrder DerivationCost

DerivationCost is a PartialOrder, not just a Preorder: antisymmetry from componentwise Nat.le_antisymm lifted by profile_injective. Mathlib's order algebra (IsAntichain, Maximal, Minimal) gets the partial-order flavor for free.

Equations

• Minimalist.instPartialOrderDerivationCost = { toPreorder := inferInstance, le_antisymm := Minimalist.instPartialOrderDerivationCost._proof_1 }

instance Minimalist.instWellFoundedLTDerivationCost : WellFoundedLT DerivationCost

The headline (Dickson's lemma applied to derivational economy): the Pareto-strict order on DerivationCost is well-founded.

Lifted from Pi.wellFoundedLT on Fin 4 → Nat — which IS Dickson's lemma applied to Nat^n — through the order embedding DerivationCost.profileEmbedding via OrderEmbedding.wellFounded.

Structural significance: this is what makes the @cite{chomsky-1995} / @cite{citko-gracanin-yuksek-2025} claim that "economy selects an optimum from the reference set" coherent. Without well-foundedness, an infinite chain c₀ > c₁ > c₂ > … of ever-more-economical derivations could exist, and "the economy winner" would be ill-defined. The well-foundedness theorem is a precondition for the linguistic content, not a corollary of it.

Mathematically: Dickson 1913, foundational for the Robbiano-Buchberger Gröbner basis termination argument and Hilbert's basis theorem on monomial ideals. The classical statement "every monomial ideal in k[x₁, …, xₙ] is finitely generated" reduces to exactly this well-foundedness on Nat^n under the divisibility order, which is the Pareto-componentwise order on exponent vectors.

theorem Minimalist.economy_admits_winner {R : Set DerivationCost} (hR : R.Nonempty) : ∃ winner ∈ R, ∀ alt ∈ R, ¬strictlyMoreEconomical alt winner

Existence of economy winners: any non-empty set R of derivation costs admits at least one Pareto-minimum — a "winner" not strictly dominated by any other element of R.

Direct corollary of WellFoundedLT DerivationCost via mathlib's WellFounded.has_min, with the < ↔ strictlyMoreEconomical translation through strictlyMoreEconomical_iff_lt.

Linguistically: the @cite{citko-gracanin-yuksek-2025} selection procedure is mathematically well-defined; whatever else economy + Pronunciation Economy + MWF do to break ties among winners, the set of winners is non-empty for any non-empty reference set.

theorem Minimalist.economy_winner_of_pair {c c' : DerivationCost} (h : strictlyMoreEconomical c c') (alt : DerivationCost) : alt ∈ {c, c'} → ¬strictlyMoreEconomical alt c

Consumer-friendly form: in a 2-element reference set {c, c'} where c strictly beats c', c is the economy winner. The common pattern in @cite{citko-gracanin-yuksek-2025}-style cost-comparison arguments: pair MD-cost vs ellipsis-cost, prove MD beats ellipsis, conclude MD is the winner.

Discharges via lt_irrefl (anti-self-domination) + asymmetry of <.

structure Minimalist.PFOperation : Type

A single PF-affecting operation: PF state immediately before vs immediately after the op fires. Used to express @cite{citko-gracanin-yuksek-2025}'s per-operation vacuity check (paper p. 27 ex (39); §3 PF reduction).

Whole-derivation Pronunciation Economy is the conjunction of per-op economy across all PF-affecting operations in the derivation.

• pfBefore : List String
• pfAfter : List String

def Minimalist.instReprPFOperation.repr : PFOperation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprPFOperation : Repr PFOperation

Equations

• Minimalist.instReprPFOperation = { reprPrec := Minimalist.instReprPFOperation.repr }

def Minimalist.instDecidableEqPFOperation.decEq (x✝ x✝¹ : PFOperation) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqPFOperation : DecidableEq PFOperation

Equations

• Minimalist.instDecidableEqPFOperation = Minimalist.instDecidableEqPFOperation.decEq

def Minimalist.PFOperation.isVacuous (op : PFOperation) : Prop

A PF operation is vacuous iff it has no effect on the PF string — e.g., the deletion targets material already unpronounced because a prior deletion removed it (paper p. 32 ex (45c)).

Equations

• op.isVacuous = (op.pfBefore = op.pfAfter)

@[implicit_reducible]

instance Minimalist.instDecidableIsVacuous (op : PFOperation) : Decidable op.isVacuous

Equations

• Minimalist.instDecidableIsVacuous op = id inferInstance

def Minimalist.pronunciationEconomy (ops : List PFOperation) : Prop

Pronunciation Economy (@cite{citko-gracanin-yuksek-2025} p. 27, ex (39)): no PF-affecting operation in the derivation is vacuous.

Crucially per-operation, not on whole-derivation PF before/after. A whole-derivation pfBefore ≠ pfAfter check under-rejects: any derivation containing one non-vacuous deletion plus N vacuous ones would pass, because the non-vacuous deletion alone ensures the whole derivation's PF changes. The paper's centerpiece argument (p. 32 ex (45c)) needs to ban exactly that configuration: a CWH structure where a shared C with E-feature deletes two TPs, the second of which is vacuous.

Equations

• Minimalist.pronunciationEconomy ops = ∀ op ∈ ops, ¬op.isVacuous

@[implicit_reducible]

instance Minimalist.instDecidablePronunciationEconomy (ops : List PFOperation) : Decidable (pronunciationEconomy ops)

Equations

• Minimalist.instDecidablePronunciationEconomy ops = id inferInstance

theorem Minimalist.pronunciationEconomy_iff_no_vacuous (ops : List PFOperation) : pronunciationEconomy ops ↔ ¬∃ op ∈ ops, op.isVacuous

Pronunciation Economy holds iff no individual operation is vacuous.

theorem Minimalist.pronunciationEconomy_violated_of_vacuous {op : PFOperation} {ops : List PFOperation} (hmem : op ∈ ops) (hvac : op.isVacuous) : ¬pronunciationEconomy ops

A derivation with any vacuous op violates Pronunciation Economy.