The Cumulativity Gap: HG ⊋ OT

[Pat09] [CP11b] [Pri02]

Harmonic Grammar with non-negative weights is strictly more expressive than Optimality Theory: every OT-realizable input→output mapping is HG-realizable (via exponentially separated weights), but the converse fails. The expressiveness gap is cumulativity — situations where the sum of multiple low-weight constraint violations exceeds a single high-weight violation. OT cannot express this; HG can.

This file states the gap as a theorem about systemic optimization problems — a single grammar must simultaneously realize a target output for every input. The single-tableau case (one input, one winner) does not exhibit the gap; the gap appears only when multiple input-output pairs constrain a shared global ranking/weighting.

Definitions

• SystemicProblem Input Output n packages multi-input optimization data: inputs, candidates per input, n-dimensional violation profile, and the target mapping the grammar must realize.
• realizedByWeighting / IsHGRealizable: existence of a non-negative weighting under which the target output strictly minimizes weighted violations for every input.
• realizedByRanking / IsOTRealizable: existence of a constraint permutation under which the target output strictly lex-dominates every alternative for every input.

Theorems

• ot_realizable_imp_hg_realizable: forward containment via exponentially separated weights (lifts lex_imp_lower_violations to the multi-input setting).
• hg_strictly_contains_ot: strict-containment witness — the abstract Lyman's Law instance (3 inputs, 2 outputs each, 3 constraints) is HG-realizable but no OT ranking realizes it.

The Lyman's Law witness comes from [CP11b] §4.2-4.3 (eq 18-19), originally [IM86] on Japanese loanword voicing. It is the smallest known witness of the cumulativity gap.

Where this is used

Studies/CoetzeePater2011.lean instantiates the abstract witness with concrete Japanese loanword forms (bobu, webbu, guddo). Future studies of HG-vs-OT cumulativity (Pater 2009 stress window cumulativity; French schwa; Tagalog nasal substitution) should likewise consume hg_strictly_contains_ot rather than re-deriving the gap per-paper.

Systemic optimization problem

structure HarmonicGrammar.SystemicProblem (Input : Type u_1) (Output : Type u_2) (n : ℕ) : Type (max u_1 u_2)

A multi-input optimization problem with a target mapping that a grammar must simultaneously realize for every input. The cumulativity gap lives here, not at the single-tableau level.

• inputs : Finset Input

  The set of inputs the grammar handles.

• cands : Input → Finset Output

  Candidate set for each input.

• vp : Input → Output → Fin n → ℕ

  Violation profile: vp i o k is the count of constraint k violations incurred by output o from input i.

• target : Input → Output

  The output the grammar must select for each input.

• target_mem (i : Input) : i ∈ self.inputs → self.target i ∈ self.cands i

  Each target output is in its input's candidate set.

def HarmonicGrammar.SystemicProblem.realizedByWeighting {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) (w : Fin n → ℝ) : Prop

A weighting w HG-realizes the target if, for every input, the target output strictly minimizes the weighted violation sum among candidates.

Equations

• P.realizedByWeighting w = ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → Constraints.weightedViolations w (P.vp i (P.target i)) < Constraints.weightedViolations w (P.vp i o)

def HarmonicGrammar.SystemicProblem.IsHGRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) : Prop

A problem is HG-realizable if some non-negative weighting realizes the target. Restricting to non-negative weights matches [Pat09]'s standard HG framework; [CP11b] §4.4 discusses the consequences of admitting negative weights (e.g., Tejano' realizability).

Equations

• P.IsHGRealizable = ∃ (w : Fin n → ℝ), (∀ (k : Fin n), 0 ≤ w k) ∧ P.realizedByWeighting w

def HarmonicGrammar.SystemicProblem.realizedByRanking {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) (σ : OptimalityTheory.Ranking n) : Prop

A constraint permutation σ OT-realizes the target if, for every input, the target output strictly lex-dominates every alternative under the ranking σ (smallest σ-index = highest-ranked constraint).

Equations

• P.realizedByRanking σ = ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → (toLex fun (k : Fin n) => P.vp i (P.target i) (σ k)) < toLex fun (k : Fin n) => P.vp i o (σ k)

def HarmonicGrammar.SystemicProblem.IsOTRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) : Prop

A problem is OT-realizable if some constraint ranking realizes the target.

Equations

• P.IsOTRealizable = ∃ (σ : OptimalityTheory.Ranking n), P.realizedByRanking σ

theorem HarmonicGrammar.SystemicProblem.realizedByRanking_iff_optimal {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] (P : SystemicProblem Input Output n) (σ : OptimalityTheory.Ranking n) : P.realizedByRanking σ ↔ ∀ (i : Input) (hi : i ∈ P.inputs), OptimalityTheory.Tableau.optimal { candidates := P.cands i, profile := fun (o : Output) => toLex fun (k : Fin n) => P.vp i o (σ k), nonempty := ⋯ } = {P.target i}

OT-realization is sole-winner per input. σ OT-realizes P iff, for every input, the target is the unique optimum of the OT tableau ranking that input's candidates by their σ-permuted violation profiles — anchoring realizedByRanking to Tableau.optimal.

Forward containment — OT ⊆ HG

theorem HarmonicGrammar.ot_realizable_imp_hg_realizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) (M : ℕ) (hM : 0 < M) (hbound : ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, ∀ (k : Fin n), P.vp i o k ≤ M) : P.IsOTRealizable → P.IsHGRealizable

Forward containment: every OT-realizable systemic problem is HG-realizable, with concrete witness given by exponentially-separated weights w(j) = (M+1)^(n-1-σ⁻¹(j)) permuted by the OT ranking.

This lifts lex_imp_lower_violations from one tableau to the multi-input setting: the same exponentially-spaced weights work uniformly for every input because the lex-dominance of the target is preserved input-wise.

Strict containment witness — abstract Lyman's Law

def HarmonicGrammar.Cumulativity.lymanVp : Fin 3 → Bool → Fin 3 → ℕ

Abstract Lyman's Law violation profile. Three constraints: F (faithfulness, e.g., IDENT-VOICE), M1 (markedness, e.g., OCP-VOICE), M2 (markedness, e.g., *VCE-GEM). Three inputs, each with two outputs (faithful = true, unfaithful = false).

input	faithful profile	unfaithful profile
0 (bobu)	[F=0, M1=1, M2=0]	[F=1, M1=0, M2=0]
1 (webbu)	[F=0, M1=0, M2=1]	[F=1, M1=0, M2=0]
2 (guddo)	[F=0, M1=1, M2=1]	[F=1, M1=0, M2=0]

Equations

• HarmonicGrammar.Cumulativity.lymanVp 0 true ⟨0, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 0 true ⟨1, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 0 true ⟨2, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 0 false ⟨0, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 0 false ⟨1, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 0 false ⟨2, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 1 true ⟨0, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 1 true ⟨1, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 1 true ⟨2, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 1 false ⟨0, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 1 false ⟨1, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 1 false ⟨2, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 2 true ⟨0, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 2 true ⟨1, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 2 true ⟨2, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 2 false ⟨0, isLt⟩ = 1
• HarmonicGrammar.Cumulativity.lymanVp 2 false ⟨1, isLt⟩ = 0
• HarmonicGrammar.Cumulativity.lymanVp 2 false ⟨2, isLt⟩ = 0

def HarmonicGrammar.Cumulativity.lymanTarget : Fin 3 → Bool

Target mapping: bobu and webbu surface faithfully (single voiced obstruent / single voiced geminate is tolerated); guddo devoices (cumulative pressure from both markedness violations exceeds the cost of a single faithfulness violation).

Equations

• HarmonicGrammar.Cumulativity.lymanTarget 0 = true
• HarmonicGrammar.Cumulativity.lymanTarget 1 = true
• HarmonicGrammar.Cumulativity.lymanTarget 2 = false

def HarmonicGrammar.Cumulativity.lymanProblem : SystemicProblem (Fin 3) Bool 3

The abstract Lyman's Law systemic problem.

Equations

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

def HarmonicGrammar.Cumulativity.lymanW : Fin 3 → ℝ

HG witness weights: [F=3, M1=2, M2=2]. Each markedness weight is individually less than F, so faithfulness wins for inputs with at most one markedness violation (bobu, webbu); the sum M1 + M2 = 4 > 3 = F overrides faithfulness for guddo.

Equations

• HarmonicGrammar.Cumulativity.lymanW ⟨0, isLt⟩ = 3
• HarmonicGrammar.Cumulativity.lymanW ⟨1, isLt⟩ = 2
• HarmonicGrammar.Cumulativity.lymanW ⟨2, isLt⟩ = 2

theorem HarmonicGrammar.Cumulativity.lyman_isHGRealizable : lymanProblem.IsHGRealizable

The abstract Lyman's Law problem is HG-realizable with weights [3,2,2].

theorem HarmonicGrammar.Cumulativity.lyman_not_isOTRealizable : ¬lymanProblem.IsOTRealizable

The abstract Lyman's Law problem is not OT-realizable: no permutation of {F, M1, M2} lex-dominates the target for all three inputs. The structural argument:

• bobu requires F to outrank M1 (else faithful loses).
• webbu requires F to outrank M2 (else faithful loses).
• guddo requires F not to be the top-ranked constraint (else unfaithful loses despite the cumulative pressure).

The first two conditions place F above both markedness constraints, contradicting the third. The proof is closed by decide over the six permutations of Fin 3 (the < on ViolationProfile is decidable).

theorem HarmonicGrammar.hg_strictly_contains_ot : ∃ (Input : Type) (Output : Type) (n : ℕ) (P : SystemicProblem Input Output n), P.IsHGRealizable ∧ ¬P.IsOTRealizable

The cumulativity gap: HG with non-negative weights strictly contains OT. Some systemic problems are HG-realizable but no OT constraint ranking realizes them. The smallest witness — abstract Lyman's Law — is provided by Cumulativity.lymanProblem.