@cite{zuraw-hayes-2017}: Intersecting Constraint Families

@cite{zuraw-hayes-2017}

@cite{zuraw-hayes-2017} "Intersecting Constraint Families: An Argument for Harmonic Grammar" (Language 93(3): 497–546).

Main claims

1. When phonological variation is governed by two independent families of constraints, the data exhibits across-the-board effects with floor and ceiling compression — a family of sigmoid curves.

2. This pattern is naturally predicted by Harmonic Grammar (MaxEnt and Noisy HG) because constraint effects are additive.

3. Decision-tree models fail because their multiplicative decomposition produces "claws" (monotonically increasing differentiation), not sigmoid families.

4. Stochastic OT fails because ranking paradoxes prevent fitting structured constraint sets to the observed pattern.

Formalization

This file develops the 2×2 sub-square of Z&H 2017's Tagalog data and proves the decision-tree failure theorem, the across-the-board consistency property of the empirical rates, and the bridge from constraint independence to the Hayes-Zuraw constant-logit-difference identity (which Z&H argue is the diagnostic of additive constraint interaction).

The 2×2 sub-square fixes two extreme cells of Z&H's full 6×6 grid (maŋ-other = highest substitution rate, paŋ-res = lowest) crossed with two of the six stem obstruents (/b/ vs /k/, voicing contrast at non-coronal places). This sub-square suffices for the mathematical content of the family-interaction argument.

The 2-way UNIFORMITY split here (unifMang, unifPang) is a restriction of Z&H's 6-way prefix-indexed UNIFORMITY constraint set (Unif-maŋ-other / Unif-maŋ-RED / Unif-maŋ-ADV / Unif-paŋ-RED / Unif-paŋ-NOUN / Unif-paŋ-RES) projected onto the maŋ-other × paŋ-res sub-grid.

Case studies (full paper)

• Tagalog nasal substitution: nearly synergistic families (both markedness and prefix UNIFORMITY constraints mostly penalize substitution; only *NC̥ favors it on the consonant side)
• French liaison/elision: synergistic families (word2 ALIGN + word1 USE both favor non-alignment)
• Hungarian vowel harmony: mixed families (stem vowel AGREE + final consonant BILABIAL/SIBILANT/etc.)

§ 1: 2×2 Square — Underlying Forms

inductive ZurawHayes2017.NasalSubInput : Type

The four underlying concatenations populating the 2×2 sub-square: two prefix constructions (maŋ-other, paŋ-res — the extreme rows of Z&H's 6-prefix grid) crossed with two stem obstruents (/b/, /k/ — the voicing contrast at non-coronal places).

• mang_b : NasalSubInput
• mang_k : NasalSubInput
• pang_b : NasalSubInput
• pang_k : NasalSubInput

@[implicit_reducible]

instance ZurawHayes2017.instDecidableEqNasalSubInput : DecidableEq NasalSubInput

Equations

• ZurawHayes2017.instDecidableEqNasalSubInput x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ZurawHayes2017.instReprNasalSubInput : Repr NasalSubInput

Equations

• ZurawHayes2017.instReprNasalSubInput = { reprPrec := ZurawHayes2017.instReprNasalSubInput.repr }

def ZurawHayes2017.instReprNasalSubInput.repr : NasalSubInput → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZurawHayes2017.instFintypeNasalSubInput : Fintype NasalSubInput

Equations

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

inductive ZurawHayes2017.NasalSubOutput : Type

The two surface variants for each underlying form.

• yes : NasalSubOutput

  YES: nasal substitution applies — nasal and obstruent coalesce.

• no : NasalSubOutput

  NO: nasal substitution does not apply — place assimilation only.

@[implicit_reducible]

instance ZurawHayes2017.instDecidableEqNasalSubOutput : DecidableEq NasalSubOutput

Equations

• ZurawHayes2017.instDecidableEqNasalSubOutput x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ZurawHayes2017.instReprNasalSubOutput : Repr NasalSubOutput

Equations

• ZurawHayes2017.instReprNasalSubOutput = { reprPrec := ZurawHayes2017.instReprNasalSubOutput.repr }

def ZurawHayes2017.instReprNasalSubOutput.repr : NasalSubOutput → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZurawHayes2017.instFintypeNasalSubOutput : Fintype NasalSubOutput

Equations

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

@[reducible, inline]

abbrev ZurawHayes2017.NasalSubCandidate : Type

Input–output pair for constraint evaluation.

Equations

• ZurawHayes2017.NasalSubCandidate = (ZurawHayes2017.NasalSubInput × ZurawHayes2017.NasalSubOutput)

def ZurawHayes2017.nasalSubSquare : Core.Constraint.Square NasalSubInput

The 2×2 square of underlying forms: prefix × stem-initial obstruent.

Equations

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

§ 2: Projection to Zuraw 2010's six-stem candidate space

Z&H §2.4 explicitly says their constraint set is "adapted from Zuraw 2010". The 4 of 6 constraints they share with Zuraw (NasSub, *NC, *[stemŋ], and the *[stemŋ]/n stringent step) are not redefined here — they're lifted from Zuraw2010 via projection. The 2 prefix-indexed UNIFORMITY constraints are Z&H's substitute for Zuraw's *ASSOC and are defined locally.

The projection maps the 4-cell sub-square onto the corresponding cells of Zuraw 2010's 6-stem × 2-decision space:

• maŋ-other + b, paŋ-res + b → (b, _)
• maŋ-other + k, paŋ-res + k → (k, _)

The prefix dimension is collapsed; the stem and yes/no dimensions are preserved.

def ZurawHayes2017.NasalSubInput.toStemC : NasalSubInput → Zuraw2010.StemC

Project a 2×2 input onto Zuraw 2010's stem consonant.

Equations

• ZurawHayes2017.NasalSubInput.mang_b.toStemC = Zuraw2010.StemC.b
• ZurawHayes2017.NasalSubInput.pang_b.toStemC = Zuraw2010.StemC.b
• ZurawHayes2017.NasalSubInput.mang_k.toStemC = Zuraw2010.StemC.k
• ZurawHayes2017.NasalSubInput.pang_k.toStemC = Zuraw2010.StemC.k

def ZurawHayes2017.NasalSubOutput.toSubSt : NasalSubOutput → Zuraw2010.SubSt

Project a 2-cell output onto Zuraw 2010's substitution decision.

Equations

• ZurawHayes2017.NasalSubOutput.yes.toSubSt = Zuraw2010.SubSt.yes
• ZurawHayes2017.NasalSubOutput.no.toSubSt = Zuraw2010.SubSt.no

def ZurawHayes2017.NasalSubCandidate.project (c : NasalSubCandidate) : Zuraw2010.NSCand

Project a Z&H candidate onto a Zuraw 2010 candidate.

Equations

• c.project = (c.1.toStemC, c.2.toSubSt)

§ 3: Constraint Inventory

The 4 shared constraints come from Zuraw 2010 via comap along the projection. The 2 prefix-indexed UNIFORMITY constraints are local.

def ZurawHayes2017.nasSub : Core.Constraint.OT.NamedConstraint NasalSubCandidate

C₁ = NasSub (markedness): per @cite{zuraw-hayes-2017} ex. (3), "Assess one violation for any nasal + obstruent sequence, where + is a morpheme boundary within a word." Lifted from Zuraw2010.nasSub.

Equations

• ZurawHayes2017.nasSub = Core.Constraint.OT.NamedConstraint.comap ZurawHayes2017.NasalSubCandidate.project Zuraw2010.nasSub

def ZurawHayes2017.starNC : Core.Constraint.OT.NamedConstraint NasalSubCandidate

C₂ = *NC: per @cite{zuraw-2010} ex. (17), "A [+nasal] segment must not be immediately followed by a [-voice, -sonorant] segment". Lifted from Zuraw2010.starNC. Violated by NO only for voiceless stems (k).

Equations

• ZurawHayes2017.starNC = Core.Constraint.OT.NamedConstraint.comap ZurawHayes2017.NasalSubCandidate.project Zuraw2010.starNC

def ZurawHayes2017.starStemVelar : Core.Constraint.OT.NamedConstraint NasalSubCandidate

C₃ = *[stemŋ]: penalizes stem-initial velar nasal. Lifted from Zuraw2010.starInitVelar. Violated by YES for k-initial stems (coalesced ŋ is velar). Z&H ex. (6c).

Equations

• ZurawHayes2017.starStemVelar = Core.Constraint.OT.NamedConstraint.comap ZurawHayes2017.NasalSubCandidate.project Zuraw2010.starInitVelar

def ZurawHayes2017.starStemVelarCoronal : Core.Constraint.OT.NamedConstraint NasalSubCandidate

C₄ = *[stemŋ]/n: penalizes stem-initial velar or coronal nasal. Lifted from Zuraw2010.starInitCorVel. In the b vs k square, this coincides with C₃ (bilabial m is neither velar nor coronal), so on the restricted domain (c.eval ∘ project) is identical for C₃ and C₄. Z&H ex. (6b).

Equations

• ZurawHayes2017.starStemVelarCoronal = Core.Constraint.OT.NamedConstraint.comap ZurawHayes2017.NasalSubCandidate.project Zuraw2010.starInitCorVel

def ZurawHayes2017.unifMang : Core.Constraint.OT.NamedConstraint NasalSubCandidate

C₅ = Unif-maŋ-other (faithfulness): one violation when the maŋ-other prefix coalesces with the stem-initial obstruent. Per Z&H ex. (5a), "One segment from input maŋ-other and a distinct input segment must not correspond to the same output segment." Restriction of Z&H's 6-way prefix-indexed UNIFORMITY family to the maŋ-other cell. Z&H-local; replaces Zuraw 2010's *ASSOC.

Equations

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

def ZurawHayes2017.unifPang : Core.Constraint.OT.NamedConstraint NasalSubCandidate

C₆ = Unif-paŋ-res (faithfulness): one violation when the paŋ-res prefix coalesces with the stem-initial obstruent. Per Z&H ex. (5f), similar to Unif-maŋ-other but for paŋ-res. Restriction of Z&H's 6-way prefix-indexed UNIFORMITY family to the paŋ-res cell.

Equations

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

def ZurawHayes2017.constraints : Fin 6 → Core.Constraint.OT.NamedConstraint NasalSubCandidate

The six constraints as a Fin 6-indexed family.

Equations

• ZurawHayes2017.constraints ⟨0, isLt⟩ = ZurawHayes2017.nasSub
• ZurawHayes2017.constraints ⟨1, isLt⟩ = ZurawHayes2017.starNC
• ZurawHayes2017.constraints ⟨2, isLt⟩ = ZurawHayes2017.starStemVelar
• ZurawHayes2017.constraints ⟨3, isLt⟩ = ZurawHayes2017.starStemVelarCoronal
• ZurawHayes2017.constraints ⟨4, isLt⟩ = ZurawHayes2017.unifMang
• ZurawHayes2017.constraints ⟨5, isLt⟩ = ZurawHayes2017.unifPang

§ 4: Violation Differences (Δₖ)

def ZurawHayes2017.violDiffProfile : Fin 6 → NasalSubInput → ℤ

Violation difference Δₖ(x) = Cₖ(x, NO) − Cₖ(x, YES) for each underlying form x and constraint k. Positive Δ favors YES.

Equations

• ZurawHayes2017.violDiffProfile ⟨0, isLt⟩ x✝ = 1
• ZurawHayes2017.violDiffProfile ⟨1, isLt⟩ ZurawHayes2017.NasalSubInput.mang_k = 1
• ZurawHayes2017.violDiffProfile ⟨1, isLt⟩ ZurawHayes2017.NasalSubInput.pang_k = 1
• ZurawHayes2017.violDiffProfile ⟨1, isLt⟩ x✝ = 0
• ZurawHayes2017.violDiffProfile ⟨2, isLt⟩ ZurawHayes2017.NasalSubInput.mang_k = -1
• ZurawHayes2017.violDiffProfile ⟨2, isLt⟩ ZurawHayes2017.NasalSubInput.pang_k = -1
• ZurawHayes2017.violDiffProfile ⟨2, isLt⟩ x✝ = 0
• ZurawHayes2017.violDiffProfile ⟨3, isLt⟩ ZurawHayes2017.NasalSubInput.mang_k = -1
• ZurawHayes2017.violDiffProfile ⟨3, isLt⟩ ZurawHayes2017.NasalSubInput.pang_k = -1
• ZurawHayes2017.violDiffProfile ⟨3, isLt⟩ x✝ = 0
• ZurawHayes2017.violDiffProfile ⟨4, isLt⟩ ZurawHayes2017.NasalSubInput.mang_b = -1
• ZurawHayes2017.violDiffProfile ⟨4, isLt⟩ ZurawHayes2017.NasalSubInput.mang_k = -1
• ZurawHayes2017.violDiffProfile ⟨4, isLt⟩ x✝ = 0
• ZurawHayes2017.violDiffProfile ⟨5, isLt⟩ ZurawHayes2017.NasalSubInput.pang_b = -1
• ZurawHayes2017.violDiffProfile ⟨5, isLt⟩ ZurawHayes2017.NasalSubInput.pang_k = -1
• ZurawHayes2017.violDiffProfile ⟨5, isLt⟩ x✝ = 0

def ZurawHayes2017.deltaR : Fin 6 → NasalSubInput → ℝ

The violation differences cast to ℝ, for use with me_predicts_hz.

Equations

• ZurawHayes2017.deltaR k x = ↑(ZurawHayes2017.violDiffProfile k x)

theorem ZurawHayes2017.violDiff_independence : Core.Constraint.ViolDiffIndependence deltaR nasalSubSquare

Violation difference independence: the violation differences Δₖ satisfy ViolDiffIndependence on the nasal substitution square.

• C₁–C₄ (markedness): Δₖ is the same for /maŋ-other+X/ and /paŋ-res+X/ (insensitive to prefix = row)
• C₅–C₆ (faithfulness): Δₖ is the same for /X+b/ and /X+k/ (insensitive to stem = column)

This is a data-level property of the constraint violation profiles, used by both Z&H's family-interaction argument and Magri 2025's MaxEnt-on-square deduction.

§ 5: Empirical Rates (2×2 square)

def ZurawHayes2017.nasalSubRate : NasalSubInput → ℚ

Empirical rates of nasal substitution from @cite{zuraw-2010}'s Tagalog dictionary type frequencies, arranged per the @cite{zuraw-hayes-2017} 2×2 sub-square. The four cells correspond to the two extreme prefixes (maŋ-other = highest rate, paŋ-res = lowest) crossed with /b/ (voiced) and /k/ (voiceless).

UNVERIFIED: bottom-row rates (0.434, 0.909) extracted from Z&H's fitted-MaxEnt tableau; should be cross-checked against the paper's Table 6 or supplementary materials before being treated as paper-citable.

Equations

• ZurawHayes2017.nasalSubRate ZurawHayes2017.NasalSubInput.mang_b = 916 / 1000
• ZurawHayes2017.nasalSubRate ZurawHayes2017.NasalSubInput.mang_k = 993 / 1000
• ZurawHayes2017.nasalSubRate ZurawHayes2017.NasalSubInput.pang_b = 434 / 1000
• ZurawHayes2017.nasalSubRate ZurawHayes2017.NasalSubInput.pang_k = 909 / 1000

§ 6: Across-the-Board Consistency

def ZurawHayes2017.ConsistentOrdering (r : Core.Constraint.Square ℚ) : Prop

Across-the-board consistency: one dimension's effect has the same sign regardless of the other dimension's value. Formally: the product of row-wise rate differences across columns is positive (same sign).

Equations

• ZurawHayes2017.ConsistentOrdering r = ((r.tl - r.bl) * (r.tr - r.br) > 0)

theorem ZurawHayes2017.tagalog_consistent_ordering : ConsistentOrdering { tl := nasalSubRate NasalSubInput.mang_b, tr := nasalSubRate NasalSubInput.mang_k, bl := nasalSubRate NasalSubInput.pang_b, br := nasalSubRate NasalSubInput.pang_k }

Tagalog nasal substitution rates exhibit across-the-board consistency: maŋ- prefixes have higher substitution than paŋ- prefixes for both voiced (/b/) and voiceless (/k/) stem-initial consonants.

§ 7: Decision-Tree Models Fail

theorem ZurawHayes2017.decision_tree_monotonic_diff (g₁ g₂ h₁ h₂ : ℚ) (hg : g₁ < g₂) (hh : h₁ < h₂) : g₁ * h₂ - g₁ * h₁ < g₂ * h₂ - g₂ * h₁

Decision-tree models predict monotonic differentiation: In a multiplicative model P(x,y) = g(x) · h(y), the difference between two h-values is proportional to g:

g(x) · h(y₂) - g(x) · h(y₁) = g(x) · (h(y₂) - h(y₁))

So at the floor (g → 0), all h-differences vanish, and at the ceiling (g → 1), h-differences are maximal. Differences grow monotonically from floor to ceiling.

This is the "claws" pattern: pinching at one end only. In contrast, MaxEnt predicts humped differentiation: sigmoid families compressed at both extremes — the observed pattern.

theorem ZurawHayes2017.decision_tree_diff_proportional (g₁ g₂ h₁ h₂ : ℚ) : (g₂ * h₂ - g₂ * h₁) * g₁ = (g₁ * h₂ - g₁ * h₁) * g₂

In a multiplicative model, the ratio of differences across two g-values exactly equals the ratio of those g-values. Cross-multiplied form (avoids division):

theorem ZurawHayes2017.decision_tree_product_bound (g h : ℚ) (hg : 0 ≤ g) (hg1 : g ≤ 1) (hh : 0 ≤ h) (hh1 : h ≤ 1) : g * h ≤ g ∧ g * h ≤ h

Decision-tree ceiling bound: in a multiplicative model with both factors in [0,1], the product is bounded above by both factors.

This is the mathematical core of why decision trees produce "claws" instead of sigmoid families: probabilities can never exceed either component probability. At the floor (g → 0), all products vanish regardless of h — explaining the pinch at one end. But at the ceiling (g → 1), differences are preserved — so there is NO compression at the top. MaxEnt, by contrast, compresses at BOTH extremes via the sigmoid function 1/(1 + eⁿ).

§ 8: Model Comparison (Table 7, Table 17)

theorem ZurawHayes2017.tagalog_maxent_best : -28482 / 100 > -29231 / 100 ∧ -28482 / 100 > -29448 / 100 ∧ -28482 / 100 > -31464 / 100 ∧ -28482 / 100 > -64572 / 100

MaxEnt achieves the best fit for Tagalog (Table 7).

theorem ZurawHayes2017.tagalog_hg_beats_ranking : -29448 / 100 > -31464 / 100 ∧ -29448 / 100 > -64572 / 100

Both HG variants beat both ranking models for Tagalog (Table 7). This is the paper's core claim: constraint weighting consistently outperforms constraint ranking.

theorem ZurawHayes2017.french_maxent_best : -19771 / 100 > -19880 / 100 ∧ -19771 / 100 > -20795 / 100 ∧ -19771 / 100 > -23361 / 100 ∧ -19771 / 100 > -41064 / 100

MaxEnt and Noisy HG achieve the best fits for French (Table 17).

theorem ZurawHayes2017.french_hg_beats_ranking : -19880 / 100 > -23361 / 100 ∧ -19880 / 100 > -41064 / 100

Both HG variants beat both ranking models for French (Table 17).

§ 9: MaxEnt Predicts the Sigmoid Family Pattern

theorem ZurawHayes2017.maxent_predicts_hz_tagalog (w : Fin 6 → ℝ) : Core.Constraint.ConstantLogitDiff (fun (x : NasalSubInput) => ∑ k : Fin 6, w k * deltaR k x) nasalSubSquare

MaxEnt predicts HZ's generalization for Tagalog nasal substitution: for any weight assignment w : Fin 6 → ℝ, the MaxEnt logit rates satisfy the constant-difference identity.

LR(/maŋb/) − LR(/maŋk/) = LR(/paŋb/) − LR(/paŋk/)

The proof instantiates me_predicts_hz (Separability.lean) with the Tagalog violation differences and their independence.

§ 10: Closed-Form Logit-Rate Difference

theorem ZurawHayes2017.hz_constant_value_tagalog (w : Fin 6 → ℚ) : ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.mang_b) - ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.mang_k) = -w 1 + w 2 + w 3

The constant logit-rate difference equals −w₂ + w₃ + w₄ for both rows, regardless of weights. This follows from the insensitivity structure of the six constraints: markedness constraints (C₁–C₄) are insensitive to prefix, so their contributions cancel in the row difference, while faithfulness constraints (C₅–C₆) are insensitive to stem consonant, so they cancel in the column difference.

theorem ZurawHayes2017.hz_constant_value_tagalog' (w : Fin 6 → ℚ) : ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.pang_b) - ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.pang_k) = -w 1 + w 2 + w 3

theorem ZurawHayes2017.hz_identity_concrete (w : Fin 6 → ℚ) : ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.mang_b) - ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.mang_k) = ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.pang_b) - ∑ k : Fin 6, w k * ↑(violDiffProfile k NasalSubInput.pang_k)

The HZ identity verified concretely: both row-differences are equal.

§ 11: NHG Produces Consistent Ordering

theorem ZurawHayes2017.nhg_consistent_ordering {X : Type} (d : X → ℝ) (σ : ℝ) (hσ : 0 < σ) (sq : Core.Constraint.Square X) (hcld : Core.Constraint.ConstantLogitDiff d sq) (hne : d sq.tl ≠ d sq.bl) : (Core.normalCDF (d sq.tl / σ) - Core.normalCDF (d sq.bl / σ)) * (Core.normalCDF (d sq.tr / σ) - Core.normalCDF (d sq.br / σ)) > 0

NHG produces consistent ordering (@cite{zuraw-hayes-2017}): when the harmony scores satisfy ConstantLogitDiff, NHG probabilities Φ(d(x)/σ) exhibit across-the-board consistency.

Composes constantLogitDiff_mono_consistent (CLD + strict monotonicity ⟹ consistent ordering) with normalCDF_strictMono. Since x ↦ Φ(x/σ) is strictly monotone for σ > 0, the result follows. This is the formal version of Z&H's argument that NHG produces sigmoid families (not claws) because the normal CDF compresses at both extremes.

theorem ZurawHayes2017.nhg_tagalog_consistent (w : Fin 6 → ℝ) (σ : ℝ) (hσ : 0 < σ) (hne : ∑ k : Fin 6, w k * deltaR k NasalSubInput.mang_b ≠ ∑ k : Fin 6, w k * deltaR k NasalSubInput.pang_b) : (Core.normalCDF ((∑ k : Fin 6, w k * deltaR k NasalSubInput.mang_b) / σ) - Core.normalCDF ((∑ k : Fin 6, w k * deltaR k NasalSubInput.pang_b) / σ)) * (Core.normalCDF ((∑ k : Fin 6, w k * deltaR k NasalSubInput.mang_k) / σ) - Core.normalCDF ((∑ k : Fin 6, w k * deltaR k NasalSubInput.pang_k) / σ)) > 0

NHG predicts consistent ordering for Tagalog nasal substitution: for any weight assignment and noise level, the NHG probabilities of nasal substitution exhibit across-the-board consistency whenever the mang- and pang- prefixes have different logit rates for b-initial stems.

End-to-end chain: Tagalog violation differences → violDiff_independence → maxent_predicts_hz_tagalog (CLD) → nhg_consistent_ordering (CDF monotonicity) → consistent ordering.

§ 12: Cross-Reference to Zuraw 2010

Z&H §2.4 says their constraint set is "adapted from Zuraw 2010". The projection-based defs in § 3 make that adaptation precise: 4 of 6 constraints are literally comap'd from Zuraw, so equality with Zuraw's constraints under projection holds by definition. The 2 prefix- indexed UNIFORMITY constraints replace Zuraw's single *ASSOC — but they turn out to be a decomposition of *ASSOC on this restricted square, not a substitution by something incompatible.

theorem ZurawHayes2017.nasSub_eq_zuraw_under_projection : nasSub.eval = Zuraw2010.nasSub.eval ∘ NasalSubCandidate.project

C₁ = NasSub agrees with Zuraw 2010 under the candidate projection. Holds by definition (comap is eval ∘ project and nasSub is defined as Zuraw2010.nasSub.comap NasalSubCandidate.project).

theorem ZurawHayes2017.starNC_eq_zuraw_under_projection : starNC.eval = Zuraw2010.starNC.eval ∘ NasalSubCandidate.project

C₂ = *NC agrees with Zuraw 2010 under the projection.

theorem ZurawHayes2017.starStemVelar_eq_zuraw_under_projection : starStemVelar.eval = Zuraw2010.starInitVelar.eval ∘ NasalSubCandidate.project

C₃ = *[stemŋ] agrees with Zuraw's starInitVelar under the projection.

theorem ZurawHayes2017.starStemVelarCoronal_eq_zuraw_under_projection : starStemVelarCoronal.eval = Zuraw2010.starInitCorVel.eval ∘ NasalSubCandidate.project

C₄ = *[stemŋ]/n agrees with Zuraw's starInitCorVel under the projection.

theorem ZurawHayes2017.unif_sum_eq_assoc (c : NasalSubCandidate) : unifMang.eval c + unifPang.eval c = Zuraw2010.starAssoc.eval c.project

Cross-paper structural insight: Z&H's prefix-indexed UNIFORMITY pair (unifMang + unifPang) is an additive decomposition of Zuraw 2010's single *ASSOC constraint on this 2×2 sub-square.

Zuraw's *ASSOC fires on every YES candidate (penalty 1) regardless of prefix. Z&H's unifMang fires on YES only for maŋ-other inputs; unifPang fires on YES only for paŋ-res inputs. On the 2×2 square, every YES cell is hit by exactly one of them, so their sum equals Zuraw's *ASSOC under the candidate projection. Under any HG/ME analysis, the sum of the two prefix-UNIF weights w₅ + w₆ plays the role Zuraw's single *ASSOC weight plays in her grammar.