The Cumulativity Gap: HG ⊋ OT

@cite{pater-2009} @cite{coetzee-pater-2011} @cite{prince-2002}

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.
• HGRealizes / IsHGRealizable: existence of a non-negative weighting under which the target output strictly minimizes weighted violations for every input.
• OTRealizes / 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 @cite{coetzee-pater-2011} §4.2-4.3 (eq 18-19), originally @cite{ito-mester-1986} on Japanese loanword voicing. It is the smallest known witness of the cumulativity gap.

Where this is used

Phenomena/Phonology/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.

@[implicit_reducible]

instance Core.Constraint.decLexStrictlyBetter {n : ℕ} (va vb : Fin n → ℕ) : Decidable (LexStrictlyBetter va vb)

LexStrictlyBetter on Fin n → ℕ is decidable: the existential ranges over Fin n, the witness predicates are over Fin with decidable equality and decidable order. Required for decide-based realizability checks on concrete instances.

Equations

• Core.Constraint.decLexStrictlyBetter va vb = id inferInstance

structure Core.Constraint.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 Core.Constraint.SystemicProblem.HGRealizes {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.HGRealizes w = ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → Core.Constraint.weightedViolations w (P.vp i (P.target i)) < Core.Constraint.weightedViolations w (P.vp i o)

def Core.Constraint.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 @cite{pater-2009}'s standard HG framework; @cite{coetzee-pater-2011} §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.HGRealizes w

def Core.Constraint.SystemicProblem.OTRealizes {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) (σ : Equiv.Perm (Fin 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

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

def Core.Constraint.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 permutation realizes the target.

Equations

• P.IsOTRealizable = ∃ (σ : Equiv.Perm (Fin n)), P.OTRealizes σ

theorem Core.Constraint.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.

def Core.Constraint.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

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

def Core.Constraint.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

• Core.Constraint.Cumulativity.lymanTarget 0 = true
• Core.Constraint.Cumulativity.lymanTarget 1 = true
• Core.Constraint.Cumulativity.lymanTarget 2 = false

def Core.Constraint.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 Core.Constraint.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

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

theorem Core.Constraint.Cumulativity.lyman_isHGRealizable : lymanProblem.IsHGRealizable

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

theorem Core.Constraint.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 (using decLexStrictlyBetter).

theorem Core.Constraint.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.