Coetzee & Pater (2011): The Place of Variation in Phonological Theory

@cite{coetzee-pater-2011}

Handbook of Phonological Theory chapter comparing three frameworks for modeling phonological variation, illustrated with English t/d-deletion.

Models formalized

1. Partially Ordered Constraints (POC) (@cite{anttila-1997}, @cite{kiparsky-1993b}): grammar is a partial order on OT constraints. Each evaluation randomly samples a total order consistent with the partial order. Probability of an output = fraction of total orders that select it as optimal.

2. MaxEnt Harmonic Grammar (@cite{goldwater-johnson-2003}): constraints have numerical weights; candidate probability ∝ exp(harmony score). More expressive than POC — can encode arbitrary probability distributions over outputs.

3. Bridge: the OT limit theorem (maxent_ot_limit) shows that as α → ∞, MaxEnt recovers OT's categorical optimization, connecting the two frameworks.

Key results

• POC deletion counts: 4! = 24 total rankings; pre-V deletion in 8, pre-pause in 8, pre-C in 12, matching @cite{coetzee-pater-2011} §3.2.

• Factorial typology: exactly 5 distinct language types across all 24 rankings, matching the 5 crucial ranking classes in table (12).

• Structural implication: every ranking that produces pre-V deletion also produces pre-C deletion. This is the formal basis for the cross-dialectal generalization pre-C ≥ pre-V.

• Tejano' impossibility (§4.4): a hypothetical dialect with pre-C < pre-V rates cannot be generated by POC or Stochastic OT but CAN be generated by MaxEnt with negative weights — a concrete framework separation theorem.

inductive Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.TDOutput : Type

Output form for t/d-deletion: either retain or delete.

• retain : TDOutput
• delete : TDOutput

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instDecidableEqTDOutput : DecidableEq TDOutput

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instDecidableEqTDOutput x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDOutput.beq : TDOutput → TDOutput → Bool

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDOutput.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDOutput : BEq TDOutput

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDOutput = { beq := Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDOutput.beq }

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDOutput : Repr TDOutput

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDOutput = { reprPrec := Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDOutput.repr }

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDOutput.repr : TDOutput → ℕ → Std.Format

Equations

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

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDOutput : Inhabited TDOutput

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDOutput = { default := Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDOutput.default }

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDOutput.default : TDOutput

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDOutput.default = Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.TDOutput.retain

structure Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.TDCandidate : Type

A candidate pairs a phonological context with an output form.

• context : Fragments.English.TDDeletion.Context
• output : TDOutput

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instDecidableEqTDCandidate : DecidableEq TDCandidate

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instDecidableEqTDCandidate = Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instDecidableEqTDCandidate.decEq

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instDecidableEqTDCandidate.decEq (x✝ x✝¹ : TDCandidate) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDCandidate.beq : TDCandidate → TDCandidate → Bool

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDCandidate.beq { context := a, output := a_1 } { context := b, output := b_1 } = (a == b && a_1 == b_1)
• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDCandidate.beq x✝¹ x✝ = false

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDCandidate : BEq TDCandidate

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDCandidate = { beq := Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instBEqTDCandidate.beq }

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDCandidate : Repr TDCandidate

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDCandidate = { reprPrec := Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDCandidate.repr }

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instReprTDCandidate.repr : TDCandidate → ℕ → Std.Format

Equations

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

instance Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDCandidate : Inhabited TDCandidate

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.instInhabitedTDCandidate = { default := { context := default, output := default } }

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.candidatesFor (ctx : Fragments.English.TDDeletion.Context) : List TDCandidate

Candidates for a given context.

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.starCT : Core.OT.NamedConstraint TDCandidate

*CT (markedness): penalizes word-final consonant clusters ending in a coronal stop. Violated by the faithful (retaining) candidate. @cite{coetzee-pater-2011} example (11).

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxC : Core.OT.NamedConstraint TDCandidate

MAX (faithfulness): penalizes deletion of an input consonant. Violated by the deleting candidate in all contexts. @cite{coetzee-pater-2011} example (11).

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxPreV : Core.OT.NamedConstraint TDCandidate

MAX-PRE-V (contextual faithfulness): penalizes deletion specifically in pre-vocalic position, where perceptual cues for t/d are maximal. @cite{coetzee-pater-2011} example (11).

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxFinal : Core.OT.NamedConstraint TDCandidate

MAX-FINAL (contextual faithfulness): penalizes deletion in phrase-final position, where consonantal release provides cues. @cite{coetzee-pater-2011} example (11).

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.constraints : List (Core.OT.NamedConstraint TDCandidate)

The four constraints from the analysis.

Equations

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

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.starCT_markedness : starCT.family = Core.OT.ConstraintFamily.markedness

*CT is a markedness constraint.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxC_faithfulness : maxC.family = Core.OT.ConstraintFamily.faithfulness

MAX is a faithfulness constraint.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxPreV_faithfulness : maxPreV.family = Core.OT.ConstraintFamily.faithfulness

MAX-PRE-V is a faithfulness constraint.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxFinal_faithfulness : maxFinal.family = Core.OT.ConstraintFamily.faithfulness

MAX-FINAL is a faithfulness constraint.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.all_violations_bounded (con : Core.OT.NamedConstraint TDCandidate) (h : con ∈ constraints) (c : TDCandidate) : con.eval c ≤ 1

All violations are bounded by 1 (binary constraints).

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.violationProfile (c : TDCandidate) : List ℕ

Violation profile for a candidate under the 4 constraints. Order: [*CT, MAX, MAX-PRE-V, MAX-FINAL].

Equations

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

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.retain_profile (ctx : Fragments.English.TDDeletion.Context) : violationProfile { context := ctx, output := TDOutput.retain } = [1, 0, 0, 0]

Retain always violates *CT once and nothing else.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.delete_preC_profile : violationProfile { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.delete } = [0, 1, 0, 0]

Delete in pre-C violates MAX only (no contextual faithfulness active).

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.delete_preV_profile : violationProfile { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.delete } = [0, 1, 1, 0]

Delete in pre-V violates MAX and MAX-PRE-V.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.delete_pause_profile : violationProfile { context := Fragments.English.TDDeletion.Context.pause, output := TDOutput.delete } = [0, 1, 0, 1]

Delete pre-pausally violates MAX and MAX-FINAL.

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.deletionOptimal (ranking : List (Core.OT.NamedConstraint TDCandidate)) (ctx : Fragments.English.TDDeletion.Context) : Bool

Check if deletion is optimal under a given ranking for a given context.

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.deletionCount (ctx : Fragments.English.TDDeletion.Context) : ℕ

Count how many of the 24 total orderings produce deletion for a context.

Equations

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

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.total_rankings : (Core.OT.permutations constraints).length = 24

Total number of rankings = 4! = 24.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.deletion_count_preV : deletionCount Fragments.English.TDDeletion.Context.preV = 8

Pre-vocalic: 8 out of 24 rankings produce deletion. Deletion requires *CT >> MAX ∧ *CT >> MAX-PRE-V.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.deletion_count_pause : deletionCount Fragments.English.TDDeletion.Context.pause = 8

Pre-pausal: 8 out of 24 rankings produce deletion. Deletion requires *CT >> MAX ∧ *CT >> MAX-FINAL.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.deletion_count_preC : deletionCount Fragments.English.TDDeletion.Context.preC = 12

Pre-consonantal: 12 out of 24 rankings produce deletion. Deletion requires only *CT >> MAX (no contextual faithfulness).

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.preC_most_deletion : deletionCount Fragments.English.TDDeletion.Context.preC > deletionCount Fragments.English.TDDeletion.Context.preV ∧ deletionCount Fragments.English.TDDeletion.Context.preC > deletionCount Fragments.English.TDDeletion.Context.pause

Pre-C deletion rate is strictly higher than pre-V and pre-pause, matching the cross-dialectal generalization.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.preV_eq_pause : deletionCount Fragments.English.TDDeletion.Context.preV = deletionCount Fragments.English.TDDeletion.Context.pause

Pre-V and pre-pause have equal deletion counts (8/24 each).

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.deletionPattern (ranking : List (Core.OT.NamedConstraint TDCandidate)) : Bool × Bool × Bool

The deletion pattern (preV?, pause?, preC?) produced by a ranking.

Equations

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

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.languageTypes : List (Bool × Bool × Bool)

The distinct language types across all 24 rankings.

Equations

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

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.factorial_typology_5_types : languageTypes.length = 5

The factorial typology has exactly 5 distinct language types, matching the 5 crucial ranking classes in table (12): a. (F,F,F) — MAX >> *CT, no deletion b. (F,T,T) — MAX-PRE-V >> *CT >> {MAX, MAX-FINAL} c. (T,F,T) — MAX-FINAL >> *CT >> {MAX, MAX-PRE-V} d. (F,F,T) — {MAX-PRE-V, MAX-FINAL} >> *CT >> MAX e. (T,T,T) — *CT >> {MAX, MAX-PRE-V, MAX-FINAL}

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.patternCount (pat : Bool × Bool × Bool) : ℕ

Helper: count rankings producing a given deletion pattern.

Equations

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

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.type_a_count : patternCount (false, false, false) = 12

Type a (F,F,F): 12 rankings — MAX >> *CT blocks all deletion.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.type_b_count : patternCount (false, true, true) = 2

Type b (F,T,T): 2 rankings — MAX-PRE-V >> *CT >> {MAX, MAX-FINAL}.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.type_c_count : patternCount (true, false, true) = 2

Type c (T,F,T): 2 rankings — MAX-FINAL >> *CT >> {MAX, MAX-PRE-V}.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.type_d_count : patternCount (false, false, true) = 2

Type d (F,F,T): 2 rankings — {MAX-PRE-V, MAX-FINAL} >> *CT >> MAX.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.type_e_count : patternCount (true, true, true) = 6

Type e (T,T,T): 6 rankings — *CT >> {MAX, MAX-PRE-V, MAX-FINAL}.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.type_counts_exhaust : patternCount (false, false, false) + patternCount (false, true, true) + patternCount (true, false, true) + patternCount (false, false, true) + patternCount (true, true, true) = 24

The 5 per-type counts sum to 24, exhausting all rankings.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.no_preV_only : patternCount (true, false, false) = 0

No ranking produces the (T,F,F) pattern — deletion only in pre-V without pre-C deletion is impossible.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.preV_deletion_implies_preC (ranking : List (Core.OT.NamedConstraint TDCandidate)) : ranking ∈ Core.OT.permutations constraints → deletionOptimal ranking Fragments.English.TDDeletion.Context.preV = true → deletionOptimal ranking Fragments.English.TDDeletion.Context.preC = true

Every ranking that produces pre-V deletion also produces pre-C deletion. This is the structural reason POC cannot generate reversed rates: pre-V deletion requires *CT >> MAX ∧ *CT >> MAX-PRE-V, which entails *CT >> MAX, the sole condition for pre-C deletion.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.pause_deletion_implies_preC (ranking : List (Core.OT.NamedConstraint TDCandidate)) : ranking ∈ Core.OT.permutations constraints → deletionOptimal ranking Fragments.English.TDDeletion.Context.pause = true → deletionOptimal ranking Fragments.English.TDDeletion.Context.preC = true

Similarly, every ranking producing pause deletion also produces pre-C deletion: *CT >> MAX ∧ *CT >> MAX-FINAL entails *CT >> MAX.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.preC_always_ge : deletionCount Fragments.English.TDDeletion.Context.preC ≥ deletionCount Fragments.English.TDDeletion.Context.preV ∧ deletionCount Fragments.English.TDDeletion.Context.preC ≥ deletionCount Fragments.English.TDDeletion.Context.pause

No ranking produces pre-V or pause deletion without also producing pre-C deletion. This is the formal basis for the cross-dialectal generalization P(del|preC) ≥ P(del|preV) in any POC grammar.

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.mkWeightedConstraints (wCT wMax wMaxPreV wMaxFin : ℚ) : List (Theories.Phonology.HarmonicGrammar.WeightedConstraint TDCandidate)

Weighted version of the t/d-deletion constraints for MaxEnt. Weight parameterization enables dialect-specific fitting.

Equations

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

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxent_deletion_preferred (wCT wMax wMaxPreV wMaxFin : ℚ) (ctx : Fragments.English.TDDeletion.Context) (h : Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := ctx, output := TDOutput.delete } > Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := ctx, output := TDOutput.retain }) : Theories.Phonology.HarmonicGrammar.moreProbable (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := ctx, output := TDOutput.delete } { context := ctx, output := TDOutput.retain }

MaxEnt harmony ordering is a decidable proxy for probability ordering: H(a) > H(b) ⟺ P(a) > P(b) by monotonicity of exp.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxent_aave_ordering : have w := mkWeightedConstraints (1006 / 10) (994 / 10) (21 / 10) (2 / 10); Theories.Phonology.HarmonicGrammar.harmonyScore w { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.delete } > Theories.Phonology.HarmonicGrammar.harmonyScore w { context := Fragments.English.TDDeletion.Context.pause, output := TDOutput.delete } ∧ Theories.Phonology.HarmonicGrammar.harmonyScore w { context := Fragments.English.TDDeletion.Context.pause, output := TDOutput.delete } > Theories.Phonology.HarmonicGrammar.harmonyScore w { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.delete }

With AAVE weights from table (23) ME-HG row, deletion probability ranks pre-C > pause > pre-V. Weights are exact ℚ transcriptions of the one-decimal-place values reported in the paper: *CT = 100.6, MAX-P-V = 2.1, MAX-FIN = 0.2, MAX = 99.4.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.nonneg_weights_preserve_ordering (wCT wMax wMaxPreV wMaxFin : ℚ) (hPreV : wMaxPreV ≥ 0) : Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.delete } ≥ Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.delete }

With non-negative MAX-PRE-V weight, harmony of pre-C deletion ≥ pre-V deletion. Pre-V delete violates {MAX, MAX-PRE-V} while pre-C delete violates only {MAX}, so H(del|preC) - H(del|preV) = wMaxPreV ≥ 0.

Banning negative weights thus makes MaxEnt respect the same typological restriction as POC (@cite{coetzee-pater-2011} §4.4).

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.nonneg_weights_preserve_ordering_pause (wCT wMax wMaxPreV wMaxFin : ℚ) (hFin : wMaxFin ≥ 0) : Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.delete } ≥ Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.pause, output := TDOutput.delete }

Analogously, non-negative MAX-FINAL weight ensures pre-C ≥ pause. H(del|preC) - H(del|pause) = wMaxFin ≥ 0.

def Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.tejanoPrime : Fragments.English.TDDeletion.Context → ℕ

Tejano' is a hypothetical dialect with reversed pre-C/pre-V rates: lowest deletion in pre-consonantal position. Created by swapping Tejano's pre-V (25%) and pre-C (62%) rates. @cite{coetzee-pater-2011} §4.4.

Equations

• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.tejanoPrime Fragments.English.TDDeletion.Context.preV = 62
• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.tejanoPrime Fragments.English.TDDeletion.Context.pause = 46
• Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.tejanoPrime Fragments.English.TDDeletion.Context.preC = 25

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.tejanoPrime_reversed : tejanoPrime Fragments.English.TDDeletion.Context.preV > tejanoPrime Fragments.English.TDDeletion.Context.preC

Tejano' has reversed rates: pre-V > pre-C.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.poc_cannot_generate_tejanoPrime : deletionCount Fragments.English.TDDeletion.Context.preC ≥ deletionCount Fragments.English.TDDeletion.Context.preV

POC cannot generate Tejano': every ranking that produces pre-V deletion also produces pre-C deletion (§7), so P(del|preC) ≥ P(del|preV) for any POC grammar over these 4 constraints.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.maxent_can_generate_tejanoPrime : ∃ (wCT : ℚ) (wMax : ℚ) (wMaxPreV : ℚ) (wMaxFin : ℚ), Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.delete } > Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.retain } ∧ Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.retain } > Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.delete } ∧ wMaxPreV < 0

MaxEnt CAN generate Tejano' with negative MAX-PRE-V weight: when MAX-PRE-V has a negative weight, violating it helps the candidate, rewarding deletion in pre-vocalic position.

Witness: *CT = 1, MAX = 2, MAX-PRE-V = -2, MAX-FINAL = 0.

• Pre-V delete: H = -(2·1 + (-2)·1) = 0; retain: H = -1
• Pre-C delete: H = -(2·1) = -2; retain: H = -1

@cite{coetzee-pater-2011} §4.4

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.framework_separation : deletionCount Fragments.English.TDDeletion.Context.preC ≥ deletionCount Fragments.English.TDDeletion.Context.preV ∧ ∃ (wCT : ℚ) (wMax : ℚ) (wMaxPreV : ℚ) (wMaxFin : ℚ), Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.delete } > Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preV, output := TDOutput.retain } ∧ Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.retain } > Theories.Phonology.HarmonicGrammar.harmonyScore (mkWeightedConstraints wCT wMax wMaxPreV wMaxFin) { context := Fragments.English.TDDeletion.Context.preC, output := TDOutput.delete }

Framework separation: POC/StOT and MaxEnt have different typological predictions. POC cannot generate all patterns that MaxEnt can.

Left conjunct: POC always has pre-C ≥ pre-V (structural implication). Right conjunct: MaxEnt can achieve pre-V > pre-C (negative weights).

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.max_dominates_implies_no_deletion (ctx : Fragments.English.TDDeletion.Context) : have ranking := [maxC, maxPreV, maxFinal, starCT]; have tab := Core.OT.buildTableau (candidatesFor ctx) ranking ⋯; tab.optimal = [{ context := ctx, output := TDOutput.retain }]

When MAX >> *CT, the categorical OT prediction is retention (no deletion) in all contexts.

theorem Phenomena.PhonologicalAlternation.Studies.CoetzeePater2011.ct_dominates_implies_deletion (ctx : Fragments.English.TDDeletion.Context) : have ranking := [starCT, maxC, maxPreV, maxFinal]; have tab := Core.OT.buildTableau (candidatesFor ctx) ranking ⋯; tab.optimal = [{ context := ctx, output := TDOutput.delete }]

When *CT >> all faithfulness, the categorical OT prediction is deletion in all contexts.