Documentation

inductive CoetzeePater2011.Context :

External phonological context following the word-final cluster. [CP11b] table (10), p. 410.

preV : Context
pause : Context
preC : Context

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instDecidableEqContext :

DecidableEq Context

Equations

CoetzeePater2011.instDecidableEqContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CoetzeePater2011.instReprContext :

Repr Context

Equations

CoetzeePater2011.instReprContext = { reprPrec := CoetzeePater2011.instReprContext.repr }

def CoetzeePater2011.instReprContext.repr :

Context → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instInhabitedContext :

Inhabited Context

Equations

CoetzeePater2011.instInhabitedContext = { default := CoetzeePater2011.instInhabitedContext.default }

@[implicit_reducible]

instance CoetzeePater2011.instFintypeContext :

Fintype Context

Equations

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

inductive CoetzeePater2011.Dialect :

English dialects with t/d-deletion data, per [CP11b] footnote 3: AAVE (Fasold 1972), Chicano (Santa Ana 1992), Jamaican (Patrick 1992), Trinidad (Kang 1994), Tejano (Bayley 1995).

aave : Dialect
chicano : Dialect
jamaican : Dialect
trinidad : Dialect
tejano : Dialect

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instDecidableEqDialect :

DecidableEq Dialect

Equations

CoetzeePater2011.instDecidableEqDialect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoetzeePater2011.instReprDialect.repr :

Dialect → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instReprDialect :

Repr Dialect

Equations

CoetzeePater2011.instReprDialect = { reprPrec := CoetzeePater2011.instReprDialect.repr }

@[implicit_reducible]

instance CoetzeePater2011.instInhabitedDialect :

Inhabited Dialect

Equations

CoetzeePater2011.instInhabitedDialect = { default := CoetzeePater2011.instInhabitedDialect.default }

@[implicit_reducible]

instance CoetzeePater2011.instFintypeDialect :

Fintype Dialect

Equations

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

def CoetzeePater2011.deletionRate :

Dialect → Context → ℕ

Observed deletion rate as a percentage (integer). From [CP11b] table (10), p. 410.

Equations

Instances For

theorem CoetzeePater2011.preC_ge_preV (d : Dialect) :

deletionRate d Context.preC ≥ deletionRate d Context.preV

Pre-consonantal deletion ≥ pre-vocalic in every dialect.

theorem CoetzeePater2011.preC_ge_pause (d : Dialect) :

deletionRate d Context.preC ≥ deletionRate d Context.pause

Pre-consonantal deletion ≥ pre-pausal in every dialect (Chicano included: 62 ≥ 37).

deletionRate Dialect.chicano Context.preV > deletionRate Dialect.chicano Context.pause

theorem CoetzeePater2011.chicano_preV_gt_pause :

Chicano is exceptional: pre-vocalic > pre-pausal.

theorem CoetzeePater2011.pause_ge_preV_non_chicano (d : Dialect) (h : d ≠ Dialect.chicano) :

deletionRate d Context.pause ≥ deletionRate d Context.preV

In all non-Chicano dialects, pre-pausal ≥ pre-vocalic.

Morphological conditioning (table 7) #

inductive CoetzeePater2011.MorphStatus :

Morphological status of the word-final t/d. [CP11b] table (7), p. 407.

regularPast : MorphStatus
semiWeakPast : MorphStatus
monomorpheme : MorphStatus

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instDecidableEqMorphStatus :

DecidableEq MorphStatus

Equations

CoetzeePater2011.instDecidableEqMorphStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoetzeePater2011.instReprMorphStatus.repr :

MorphStatus → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instReprMorphStatus :

Repr MorphStatus

Equations

CoetzeePater2011.instReprMorphStatus = { reprPrec := CoetzeePater2011.instReprMorphStatus.repr }

@[implicit_reducible]

instance CoetzeePater2011.instFintypeMorphStatus :

Fintype MorphStatus

Equations

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

inductive CoetzeePater2011.MorphDialect :

Dialect labels for table (7) morphological data. Table (7) uses different dialects than table (10) — Philadelphia English replaces AAVE; Jamaican and Trinidad have no morph data.

philadelphia : MorphDialect
chicano : MorphDialect
tejano : MorphDialect

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instDecidableEqMorphDialect :

DecidableEq MorphDialect

Equations

CoetzeePater2011.instDecidableEqMorphDialect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoetzeePater2011.instReprMorphDialect.repr :

MorphDialect → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instReprMorphDialect :

Repr MorphDialect

Equations

CoetzeePater2011.instReprMorphDialect = { reprPrec := CoetzeePater2011.instReprMorphDialect.repr }

@[implicit_reducible]

instance CoetzeePater2011.instFintypeMorphDialect :

Fintype MorphDialect

Equations

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

def CoetzeePater2011.morphDeletionRate :

MorphDialect → MorphStatus → ℕ

Deletion rate by morphological status and dialect (percentages). From [CP11b] table (7).

Equations

Instances For

theorem CoetzeePater2011.mono_ge_regular (d : MorphDialect) :

morphDeletionRate d MorphStatus.monomorpheme ≥ morphDeletionRate d MorphStatus.regularPast

Monomorpheme deletion ≥ regular past in every dialect with data.

theorem CoetzeePater2011.semiWeak_ge_regular (d : MorphDialect) :

morphDeletionRate d MorphStatus.semiWeakPast ≥ morphDeletionRate d MorphStatus.regularPast

Semi-weak past ≥ regular past in every dialect with data.

theorem CoetzeePater2011.mono_ge_semiWeak (d : MorphDialect) :

morphDeletionRate d MorphStatus.monomorpheme ≥ morphDeletionRate d MorphStatus.semiWeakPast

Monomorpheme deletion ≥ semi-weak past in every dialect with data. Together with semiWeak_ge_regular, this discharges Guy 1991b's three-way ordering monomorpheme ≥ semi-weak ≥ regular past.

Candidate type #

inductive CoetzeePater2011.TDOutput :

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

retain : TDOutput
delete : TDOutput

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instDecidableEqTDOutput :

DecidableEq TDOutput

Equations

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

@[implicit_reducible]

instance CoetzeePater2011.instReprTDOutput :

Repr TDOutput

Equations

CoetzeePater2011.instReprTDOutput = { reprPrec := CoetzeePater2011.instReprTDOutput.repr }

def CoetzeePater2011.instReprTDOutput.repr :

TDOutput → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instInhabitedTDOutput :

Inhabited TDOutput

Equations

CoetzeePater2011.instInhabitedTDOutput = { default := CoetzeePater2011.instInhabitedTDOutput.default }

@[implicit_reducible]

instance CoetzeePater2011.instFintypeTDOutput :

Fintype TDOutput

Equations

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

structure CoetzeePater2011.TDCandidate :

A candidate pairs a phonological context with an output form.

context : Context
output : TDOutput

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instDecidableEqTDCandidate :

DecidableEq TDCandidate

Equations

CoetzeePater2011.instDecidableEqTDCandidate = CoetzeePater2011.instDecidableEqTDCandidate.decEq

def CoetzeePater2011.instDecidableEqTDCandidate.decEq (x✝ x✝¹ : TDCandidate) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def CoetzeePater2011.instReprTDCandidate.repr :

TDCandidate → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance CoetzeePater2011.instReprTDCandidate :

Repr TDCandidate

Equations

CoetzeePater2011.instReprTDCandidate = { reprPrec := CoetzeePater2011.instReprTDCandidate.repr }

@[implicit_reducible]

instance CoetzeePater2011.instInhabitedTDCandidate :

Inhabited TDCandidate

Equations

CoetzeePater2011.instInhabitedTDCandidate = { default := { context := default, output := default } }

def CoetzeePater2011.candidatesFor (ctx : Context) :

List TDCandidate

Candidates for a given context.

Equations

CoetzeePater2011.candidatesFor ctx = [{ context := ctx, output := CoetzeePater2011.TDOutput.retain }, { context := ctx, output := CoetzeePater2011.TDOutput.delete }]

Instances For

Constraints (example 11) #

def CoetzeePater2011.starCT :

*CT (markedness): penalizes word-final consonant clusters ending in a coronal stop. Violated by the faithful (retaining) candidate. [CP11b] example (11).

Equations

CoetzeePater2011.starCT = Constraints.Constraint.binary fun (c : CoetzeePater2011.TDCandidate) => (c.output == CoetzeePater2011.TDOutput.retain) = true

Instances For

def CoetzeePater2011.maxC :

MAX (faithfulness): penalizes deletion of an input consonant. Violated by the deleting candidate in all contexts. [CP11b] example (11).

Equations

CoetzeePater2011.maxC = Constraints.Constraint.binary fun (c : CoetzeePater2011.TDCandidate) => (c.output == CoetzeePater2011.TDOutput.delete) = true

Instances For

def CoetzeePater2011.maxPreV :

MAX-PRE-V (contextual faithfulness): penalizes deletion specifically in pre-vocalic position, where perceptual cues for t/d are maximal. [CP11b] example (11).

Equations

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

Instances For

def CoetzeePater2011.maxFinal :

MAX-FINAL (contextual faithfulness): penalizes deletion in phrase-final position, where consonantal release provides cues. [CP11b] example (11).

Equations

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

Instances For

def CoetzeePater2011.constraints :

List (Constraints.Constraint TDCandidate)

The four constraints from the analysis.

Equations

CoetzeePater2011.constraints = [CoetzeePater2011.starCT, CoetzeePater2011.maxC, CoetzeePater2011.maxPreV, CoetzeePater2011.maxFinal]

Instances For

theorem CoetzeePater2011.all_violations_bounded (con : Constraints.Constraint TDCandidate) (h : con ∈ constraints) (c : TDCandidate) :

con c ≤ 1

All violations are bounded by 1 (binary constraints).

Violation profiles #

def CoetzeePater2011.violationProfile (c : TDCandidate) :

List ℕ

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

Equations

CoetzeePater2011.violationProfile c = List.map (fun (con : Constraints.Constraint CoetzeePater2011.TDCandidate) => con c) CoetzeePater2011.constraints

Instances For

theorem CoetzeePater2011.retain_profile (ctx : Context) :

violationProfile { context := ctx, output := TDOutput.retain } = [1, 0, 0, 0]

Retain always violates *CT once and nothing else.

theorem CoetzeePater2011.delete_preC_profile :

violationProfile { context := Context.preC, output := TDOutput.delete } = [0, 1, 0, 0]

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

theorem CoetzeePater2011.delete_preV_profile :

violationProfile { context := Context.preV, output := TDOutput.delete } = [0, 1, 1, 0]

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

theorem CoetzeePater2011.delete_pause_profile :

violationProfile { context := Context.pause, output := TDOutput.delete } = [0, 1, 0, 1]

Delete pre-pausally violates MAX and MAX-FINAL.

POC adapter: `tdCands` and `tdVp` for `pocPredict` consumption #

def CoetzeePater2011.tdCands :

Context → Finset TDOutput

Candidate set per context for POC: both retain and delete are available in every context. Required by PartialOrderConstraints.pocPredict.

Equations

CoetzeePater2011.tdCands x✝ = Finset.univ

Instances For

def CoetzeePater2011.tdVp :

Context → TDOutput → Fin 4 → ℕ

Violation profile in POC's Input → Output → Fin n → ℕ shape. Constraint indexing matches constraints: 0 = *CT, 1 = MAX, 2 = MAX-PRE-V, 3 = MAX-FINAL.

Equations

CoetzeePater2011.tdVp x✝ CoetzeePater2011.TDOutput.retain ⟨0, isLt⟩ = 1
CoetzeePater2011.tdVp x✝ CoetzeePater2011.TDOutput.delete ⟨1, isLt⟩ = 1
CoetzeePater2011.tdVp CoetzeePater2011.Context.preV CoetzeePater2011.TDOutput.delete ⟨2, isLt⟩ = 1
CoetzeePater2011.tdVp CoetzeePater2011.Context.pause CoetzeePater2011.TDOutput.delete ⟨3, isLt⟩ = 1
CoetzeePater2011.tdVp x✝² x✝¹ x✝ = 0

Instances For

POC model — substrate-derived #

[CP11b] §3.2 explicitly adopts the POC framework: "the grammar states a partial, rather than a total, order on the constraint set. Each time the grammar is used to evaluate a candidate set, one of the total orders consistent with the partial order is randomly chosen." Equation (9): "If a candidate is selected as optimal in n of these rankings, then this candidate's probability of occurrence is n/t."

We formalize the §3.2 t/d-deletion analysis (table 10) using POC's
`pocPredict`, with deletion probabilities derived in closed form via
the `picksAt_binary_iff_permDList_head_lt` bridge + the substrate's
`perm_filter_head_in_card`.

The discrete partial order (`PartialOrderConstraints.discrete 4`)
encodes "no rankings imposed" — uniform sampling over all 4! = 24
total orders.

def CoetzeePater2011.deletionProb (ctx : Context) :

ℚ

Probability that POC sampling selects deletion at context ctx, under the discrete partial order.

Equations

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

Instances For

theorem CoetzeePater2011.deletionProb_preV :

deletionProb Context.preV = 1 / 3

Pre-vocalic deletion probability: D = {*CT, MAX, MAX-PRE-V} (3 distinguishing), Y ∩ D = {*CT} (only *CT favors delete) → 1/3.

theorem CoetzeePater2011.deletionProb_pause :

deletionProb Context.pause = 1 / 3

Phrase-final deletion probability: D = {*CT, MAX, MAX-FINAL}, Y ∩ D = {*CT} → 1/3.

theorem CoetzeePater2011.deletionProb_preC :

deletionProb Context.preC = 1 / 2

Pre-consonantal deletion probability: D = {*CT, MAX}, Y ∩ D = {*CT} → 1/2 (highest — no positional faithfulness applies).

theorem CoetzeePater2011.deletionProb_preC_gt :

deletionProb Context.preC > deletionProb Context.preV ∧ deletionProb Context.preC > deletionProb Context.pause

The cross-dialectal generalization: pre-C deletion rate exceeds pre-V and pre-pause rates. Direct consequence of the closed-form arithmetic — no enumeration.

deletionProb Context.preV = deletionProb Context.pause

theorem CoetzeePater2011.deletionProb_preV_eq_pause :

Pre-V and pre-pause have equal deletion probabilities (1/3 each).

Factorial typology (table 12) — POC-native #

The factorial typology over Equiv.Perm (Fin 4) rankings, using POC's PicksAt for the per-context deletion check. Per-σ pattern is (PicksAt σ .preV .delete, PicksAt σ .pause .delete, PicksAt σ .preC .delete).

These are per-σ patterns (not head-in-Y predicates), so the substrate
doesn't apply — we use plain `decide` on the 24-perm `Equiv.Perm (Fin 4)`.

def CoetzeePater2011.deletionPattern (σ : Equiv.Perm (Fin 4)) :

Bool × Bool × Bool

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

Equations

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

Instances For

def CoetzeePater2011.factorialTypes :

Finset (Bool × Bool × Bool)

Distinct categorical dialect types over all 4! = 24 total orders.

Equations

CoetzeePater2011.factorialTypes = Finset.image CoetzeePater2011.deletionPattern Finset.univ

Instances For

theorem CoetzeePater2011.factorial_typology_5_types :

factorialTypes.card = 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}

theorem CoetzeePater2011.type_a_count :

{σ : Equiv.Perm (Fin 4) | deletionPattern σ = (false, false, false)}.card = 12

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

theorem CoetzeePater2011.type_b_count :

{σ : Equiv.Perm (Fin 4) | deletionPattern σ = (false, true, true)}.card = 2

Type b (F,T,T): 2 rankings.

theorem CoetzeePater2011.type_c_count :

{σ : Equiv.Perm (Fin 4) | deletionPattern σ = (true, false, true)}.card = 2

Type c (T,F,T): 2 rankings.

theorem CoetzeePater2011.type_d_count :

{σ : Equiv.Perm (Fin 4) | deletionPattern σ = (false, false, true)}.card = 2

Type d (F,F,T): 2 rankings.

theorem CoetzeePater2011.type_e_count :

{σ : Equiv.Perm (Fin 4) | deletionPattern σ = (true, true, true)}.card = 6

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

theorem CoetzeePater2011.no_preV_only :

{σ : Equiv.Perm (Fin 4) | deletionPattern σ = (true, false, false)}.card = 0

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

Structural implication (key POC typological prediction) #

theorem CoetzeePater2011.preV_deletion_implies_preC (σ : Equiv.Perm (Fin 4)) :

HarmonicGrammar.PartialOrderConstraints.PicksAt tdCands tdVp σ Context.preV TDOutput.delete → HarmonicGrammar.PartialOrderConstraints.PicksAt tdCands tdVp σ Context.preC TDOutput.delete

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 CoetzeePater2011.pause_deletion_implies_preC (σ : Equiv.Perm (Fin 4)) :

HarmonicGrammar.PartialOrderConstraints.PicksAt tdCands tdVp σ Context.pause TDOutput.delete → HarmonicGrammar.PartialOrderConstraints.PicksAt tdCands tdVp σ Context.preC TDOutput.delete

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

theorem CoetzeePater2011.preC_always_ge :

deletionProb Context.preC ≥ deletionProb Context.preV ∧ deletionProb Context.preC ≥ deletionProb Context.pause

No ranking produces pre-V or pause deletion without also producing pre-C deletion. The formal basis for the cross-dialectal generalization P(del|preC) ≥ P(del|preV). Direct corollary of the closed-form deletionProb_* theorems.

MaxEnt model #

def CoetzeePater2011.tdCon :

Constraints.CON TDCandidate 4

The four t/d-deletion constraints as a CON (constraint vector) for MaxEnt. Index order matches constraints: 0 = *CT, 1 = MAX, 2 = MAX-PRE-V, 3 = MAX-FINAL.

Equations

CoetzeePater2011.tdCon = ![CoetzeePater2011.starCT, CoetzeePater2011.maxC, CoetzeePater2011.maxPreV, CoetzeePater2011.maxFinal]

Instances For

def CoetzeePater2011.tdW (wCT wMax wMaxPreV wMaxFin : ℝ) :

Fin 4 → ℝ

MaxEnt weight vector for tdCon, in the same [*CT, MAX, MAX-PRE-V, MAX-FINAL] order. Weight parameterization enables dialect-specific fitting.

Equations

CoetzeePater2011.tdW wCT wMax wMaxPreV wMaxFin = ![wCT, wMax, wMaxPreV, wMaxFin]

Instances For

theorem CoetzeePater2011.maxent_deletion_preferred (wCT wMax wMaxPreV wMaxFin : ℝ) (ctx : Context) (h : Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := ctx, output := TDOutput.delete } > Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := ctx, output := TDOutput.retain }) :

Constraints.harmonyDominates tdCon (tdW 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 CoetzeePater2011.maxent_aave_ordering :

have w := tdW (1006 / 10) (994 / 10) (21 / 10) (2 / 10); Constraints.harmonyScore tdCon w { context := Context.preC, output := TDOutput.delete } > Constraints.harmonyScore tdCon w { context := Context.pause, output := TDOutput.delete } ∧ Constraints.harmonyScore tdCon w { context := Context.pause, output := TDOutput.delete } > Constraints.harmonyScore tdCon w { context := 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 CoetzeePater2011.nonneg_weights_preserve_ordering (wCT wMax wMaxPreV wMaxFin : ℝ) (hPreV : wMaxPreV ≥ 0) :

Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preC, output := TDOutput.delete } ≥ Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := 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 ([CP11b] §4.4).

theorem CoetzeePater2011.nonneg_weights_preserve_ordering_pause (wCT wMax wMaxPreV wMaxFin : ℝ) (hFin : wMaxFin ≥ 0) :

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

Tejano' impossibility #

def CoetzeePater2011.tejanoPrime :

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. [CP11b] §4.4.

Equations

Instances For

tejanoPrime Context.preV > tejanoPrime Context.preC

theorem CoetzeePater2011.tejanoPrime_reversed :

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

theorem CoetzeePater2011.poc_cannot_generate_tejanoPrime :

deletionProb Context.preC ≥ deletionProb 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 CoetzeePater2011.maxent_can_generate_tejanoPrime :

∃ (wCT : ℝ) (wMax : ℝ) (wMaxPreV : ℝ) (wMaxFin : ℝ), Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preV, output := TDOutput.delete } > Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preV, output := TDOutput.retain } ∧ Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preC, output := TDOutput.retain } > Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := 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 from [CP11b] table (23) Tejano' ME-HG row: *CT = 99.4, MAX = 100.6, MAX-PRE-V = −1.6, MAX-FINAL = −0.8. These are the weights the paper's MaxEnt fitting procedure learned on Tejano' frequencies.

Witness arithmetic:

Pre-V delete: H = −(100.6·1 + (−1.6)·1) = −99
Pre-V retain: H = −(99.4·1) = −99.4 → delete > retain ✓
Pre-C delete: H = −(100.6·1) = −100.6
Pre-C retain: H = −(99.4·1) = −99.4 → retain > delete ✓ (REVERSED)

[CP11b] §4.4, table (23)

theorem CoetzeePater2011.framework_separation :

deletionProb Context.preC ≥ deletionProb Context.preV ∧ ∃ (wCT : ℝ) (wMax : ℝ) (wMaxPreV : ℝ) (wMaxFin : ℝ), Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preV, output := TDOutput.delete } > Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preV, output := TDOutput.retain } ∧ Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := Context.preC, output := TDOutput.retain } > Constraints.harmonyScore tdCon (tdW wCT wMax wMaxPreV wMaxFin) { context := 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).

Categorical OT bookends #

theorem CoetzeePater2011.max_dominates_implies_no_deletion (ctx : Context) :

have ranking := [maxC, maxPreV, maxFinal, starCT]; have tab := OptimalityTheory.Tableau.ofRanking (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 CoetzeePater2011.ct_dominates_implies_deletion (ctx : Context) :

have ranking := [starCT, maxC, maxPreV, maxFinal]; have tab := OptimalityTheory.Tableau.ofRanking (candidatesFor ctx) ranking ⋯; tab.optimal = {{ context := ctx, output := TDOutput.delete }}

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

Generic ConstraintSystem predictions (per-context MaxEnt) #

At each context, the AAVE MaxEnt model is a per-context ConstraintSystem TDOutput ℝ: candidates = {retain, delete}, score = harmony of (ctx, ·), decoder = softmaxDecoder 1. The two-candidate softmax is the logistic function, so predict .delete is genuine conditional probability P(delete | ctx).

noncomputable def CoetzeePater2011.aaveW :

Fin 4 → ℝ

The AAVE constraint weights from table (23) ME-HG row.

Equations

CoetzeePater2011.aaveW = CoetzeePater2011.tdW (1006 / 10) (994 / 10) (21 / 10) (2 / 10)

Instances For

noncomputable def CoetzeePater2011.aaveSystem (ctx : Context) :

Core.Optimization.ConstraintSystem TDOutput ℝ

The AAVE MaxEnt model at a fixed context, packaged as a generic ConstraintSystem. With only two candidates, predict .delete is the conditional probability P(delete | ctx).

Equations

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

Instances For

theorem CoetzeePater2011.aave_preC_prefers_delete :

(aaveSystem Context.preC).predict TDOutput.retain < (aaveSystem Context.preC).predict TDOutput.delete

In the pre-consonantal context, the AAVE system predicts deletion over retention. Conditional probability claim: P(delete | preC) > P(retain | preC).

theorem CoetzeePater2011.aave_preV_prefers_retain :

(aaveSystem Context.preV).predict TDOutput.delete < (aaveSystem Context.preV).predict TDOutput.retain

In the pre-vocalic context, the AAVE system predicts retention over deletion: pre-V deletion violates both MAX and MAX-PRE-V, costing more than the *CT violation incurred by retention. Conditional probability claim: P(retain | preV) > P(delete | preV).