Storme (2026) [Sto26b]

A method to evaluate systemic constraints in probabilistic grammars: systemic constraints — *Homophony and others that score several input–output mappings jointly — become compatible with probabilistic grammars by evaluating a MaxEnt distribution over joint output tuples and marginalizing to recover individual mapping probabilities. The case study is variable hiatus in spoken Persian ([AJ21]): the suffix vowel deletes freely in /hutʃɑ-emun/ (1PL possessive) but rarely in /hutʃɑ-e/ (definite), where deletion would leave the suffixed form homophonous with the bare stem. This file builds the paradigm from two Hiatus.Junctures over Persian segments — homophony is string identity, and the suffix-length conditioning is string algebra (baseCollisions_eq) — and derives the closed form of the marginalized model (persianMarginal_eq_softmax), its fitted-weight preference orders (Table 5), and the suffix-length effect that *Homophony creates (homophony_length_effect) and classical constraints cannot (classical_no_length_effect).

Systemic Constraints

@[reducible, inline]

abbrev Storme2026.SystemicConstraint (n : ℕ) (O : Type u_1) : Type u_1

A systemic constraint evaluates a whole output tuple — one output per input — rather than an individual input→output pair, so it cannot be decomposed into per-mapping evaluations (e.g. *HOMOPHONY counts colliding output pairs). Like a Constraint, it is its violation-counting function; its weight is supplied separately (the systemic twin of an HG weight).

Equations

• Storme2026.SystemicConstraint n O = ((Fin n → O) → ℕ)

def Storme2026.homophonyAvoidance {n : ℕ} {O : Type u_1} [DecidableEq O] : SystemicConstraint n O

*HOMOPHONY: penalizes output tuples where distinct inputs receive the same output, counting the colliding pairs |{(i, j) : i < j ∧ f i = f j}|.

Equations

• Storme2026.homophonyAvoidance f = {p : Fin n × Fin n | p.1 < p.2 ∧ f p.1 = f p.2}.card

theorem Storme2026.homophonyAvoidance_pair {O : Type u_1} [DecidableEq O] (a b : O) : homophonyAvoidance ![a, b] = if a = b then 1 else 0

On a two-item paradigm, *HOMOPHONY is the collision indicator.

Joint Distribution with Systemic Constraints

def Storme2026.systemicScore {n k : ℕ} {O : Type u_1} (sw : Fin k → ℝ) (scon : Fin k → SystemicConstraint n O) (f : Fin n → O) : ℝ

Systemic harmony of an output tuple: -∑ⱼ swⱼ · sconⱼ(f), the negated weighted sum of the systemic constraints' tuple-violation counts. The systemic twin of harmonyScore — same negated-weighted-sum shape, but scoring whole tuples; it is the coupling component of the joint score.

Equations

• Storme2026.systemicScore sw scon f = -∑ j : Fin k, sw j * ↑(scon j f)

noncomputable def Storme2026.jointHarmonyScore {n m k : ℕ} {I : Type u_1} {O : Type u_2} (inputs : Fin n → I) (classicalCon : Constraints.CON (I × O) m) (classicalW : Fin m → ℝ) (sw : Fin k → ℝ) (scon : Fin k → SystemicConstraint n O) (f : Fin n → O) : ℝ

Joint harmony score over the product space, combining classical per-mapping scores with the systemic tuple-level score: H_joint(f) = ∑ᵢ H(iᵢ, f i) + systemicScore sw scon f.

Equations

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

noncomputable def Storme2026.maxEntCoupled {n m k : ℕ} {I : Type u_1} {O : Type u_2} [Fintype O] [DecidableEq O] (inputs : Fin n → I) (classicalCon : Constraints.CON (I × O) m) (classicalW : Fin m → ℝ) (sw : Fin k → ℝ) (scon : Fin k → SystemicConstraint n O) : CoupledSoftmax (Fin n) O

MaxEnt grammar with systemic constraints as a CoupledSoftmax: componentScore i v = harmonyScore classicalCon classicalW (inputs i, v) and couplingScore f = systemicScore sw scon f. The joint probability is a softmax over all Fin n → O output tuples; its marginal at position i recovers the individual mapping probability under systemic pressure.

Equations

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

noncomputable def Storme2026.marginalProb {n m k : ℕ} {I : Type u_1} {O : Type u_2} [Fintype O] [DecidableEq O] [Nonempty O] (inputs : Fin n → I) (classicalCon : Constraints.CON (I × O) m) (classicalW : Fin m → ℝ) (sw : Fin k → ℝ) (scon : Fin k → SystemicConstraint n O) (i : Fin n) (o : O) : ℝ

Marginal probability P(oᵢ ∣ iᵢ) = ∑_{f : f i = oᵢ} P_joint(f): marginalize the joint distribution to recover a specific mapping's probability under systemic pressure ([Sto26b]'s key equation). Defined through CoupledSoftmax.marginal so that factorization follows from marginal_eq_independent_when_uncoupled.

Equations

• Storme2026.marginalProb inputs classicalCon classicalW sw scon i o = (Storme2026.maxEntCoupled inputs classicalCon classicalW sw scon).marginal i o

Factorization Theorem

theorem Storme2026.marginal_eq_classical_when_no_systemic {n m k : ℕ} {I : Type u_1} {O : Type u_2} [Fintype O] [DecidableEq O] [Nonempty O] (inputs : Fin n → I) (classicalCon : Constraints.CON (I × O) m) (classicalW : Fin m → ℝ) (sw : Fin k → ℝ) (scon : Fin k → SystemicConstraint n O) (h_zero : ∀ (j : Fin k), sw j = 0) (i : Fin n) (o : O) : marginalProb inputs classicalCon classicalW sw scon i o = softmax (fun (o' : O) => Constraints.harmonyScore classicalCon classicalW (inputs i, o')) o

Factorization: when systemic weights are all zero, the marginal equals the classical MaxEnt probability. The coupling score is then constant (= 0), so marginal_eq_independent_when_uncoupled applies: the joint factorizes and each marginal equals its independent per-item softmax.

The paradigm: two junctures, three candidate resolutions

inductive Storme2026.Resolution : Type

The three candidate resolutions [AJ21] consider for a suffixed input — the paper's restriction of the hiatus-resolution typology ([Cas11b]).

• hiatus : Resolution

  Faithful vowel hiatus, e.g. [hutʃɑe].

• epenthesis : Resolution

  Glottal-stop epenthesis, e.g. [hutʃɑʔe].

• deletion : Resolution

  Suffix-vowel deletion, e.g. [hutʃɑ], [hutʃɑmun].

@[instance_reducible]

instance Storme2026.instDecidableEqResolution : DecidableEq Resolution

Equations

• Storme2026.instDecidableEqResolution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Storme2026.instFintypeResolution : Fintype Resolution

Equations

• Storme2026.instFintypeResolution = { elems := { val := ↑Storme2026.Resolution.enumList, nodup := Storme2026.Resolution.enumList_nodup }, complete := Storme2026.instFintypeResolution._proof_1 }

@[instance_reducible]

instance Storme2026.instInhabitedResolution : Inhabited Resolution

Equations

• Storme2026.instInhabitedResolution = { default := Storme2026.instInhabitedResolution.default }

@[instance_reducible]

instance Storme2026.instReprResolution : Repr Resolution

Equations

• Storme2026.instReprResolution = { reprPrec := Storme2026.instReprResolution.repr }

def Storme2026.instReprResolution.repr : Resolution → ℕ → Std.Format

Equations

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

instance Storme2026.instNontrivialResolution : Nontrivial Resolution

def Storme2026.definite : Phonology.Hiatus.Juncture

The definite-suffix juncture /hutʃɑ-e/: monosegmental suffix.

Equations

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

def Storme2026.possessive : Phonology.Hiatus.Juncture

The possessive-suffix juncture /hutʃɑ-emun/: polysegmental suffix.

Equations

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

def Storme2026.inputs : Fin 2 → Phonology.Hiatus.Juncture

The joint tableau's inputs, indexed for marginalProb.

Equations

• Storme2026.inputs = ![Storme2026.definite, Storme2026.possessive]

def Storme2026.stem : List Phonology.Segment

The bare stem [hutʃɑ].

Equations

• Storme2026.stem = Storme2026.definite.stem

def Storme2026.resolve : Resolution → Phonology.Hiatus.Juncture → List Phonology.Segment

Each candidate as a Hiatus.Juncture repair: faithful hiatus, glottal-stop epenthesis, V2 elision.

Equations

• Storme2026.resolve Storme2026.Resolution.hiatus = Phonology.Hiatus.Juncture.input
• Storme2026.resolve Storme2026.Resolution.epenthesis = fun (x : Phonology.Hiatus.Juncture) => x.epenthesize Farsi.Phonology.glottal
• Storme2026.resolve Storme2026.Resolution.deletion = Phonology.Hiatus.Juncture.elideV2

theorem Storme2026.resolve_deletion_definite : resolve Resolution.deletion definite = stem

[hutʃɑ]: deletion at the monosegmental juncture is the bare stem — the concrete instance of Hiatus.Juncture.elideV2_eq_stem_iff.

theorem Storme2026.resolve_deletion_possessive_ne_stem : resolve Resolution.deletion possessive ≠ stem

[hutʃɑmun]: deletion at the polysegmental juncture keeps a residue distinct from the stem.

Constraints computed on strings, and the fitted weights

def Storme2026.starHiatus : Constraints.Constraint (Phonology.Hiatus.Juncture × Resolution)

*Hiatus: vowel–vowel adjacencies surviving in the surface form.

Equations

• Storme2026.starHiatus c = Phonology.Hiatus.count (Storme2026.resolve c.2 c.1)

def Storme2026.depConstraint : Constraints.Constraint (Phonology.Hiatus.Juncture × Resolution)

Dep: inserted segments — the surface form's length excess over the input. Length-based counting is exact for this candidate set, since every candidate differs from the input by pure insertion or pure deletion.

Equations

• Storme2026.depConstraint c = (Storme2026.resolve c.2 c.1).length - c.1.input.length

def Storme2026.maxConstraint : Constraints.Constraint (Phonology.Hiatus.Juncture × Resolution)

Max: deleted segments — the input's length excess over the surface form.

Equations

• Storme2026.maxConstraint c = c.1.input.length - (Storme2026.resolve c.2 c.1).length

theorem Storme2026.depConstraint_eq (j : Phonology.Hiatus.Juncture) (o : Resolution) : depConstraint (j, o) = if o = Resolution.epenthesis then 1 else 0

Dep's string count reproduces its binary Table 4 column — for any juncture.

theorem Storme2026.maxConstraint_eq (j : Phonology.Hiatus.Juncture) (o : Resolution) : maxConstraint (j, o) = if o = Resolution.deletion then 1 else 0

Max's string count reproduces its binary Table 4 column — for any juncture.

theorem Storme2026.starHiatus_eq (k : Fin 2) (o : Resolution) : starHiatus (inputs k, o) = if o = Resolution.hiatus then 1 else 0

*Hiatus's string count reproduces its binary Table 4 column on the paradigm's junctures. Unlike Dep and Max this depends on their segmental content: hiatus must survive nowhere but the juncture itself.

def Storme2026.classicalCon : Constraints.CON (Phonology.Hiatus.Juncture × Resolution) 3

The classical (per-mapping) constraint vector: Dep, *Hiatus, Max.

Equations

• Storme2026.classicalCon = ![Storme2026.depConstraint, Storme2026.starHiatus, Storme2026.maxConstraint]

noncomputable def Storme2026.classicalW : Fin 3 → ℝ

Fitted weights (posterior means) from [Sto26b]'s Table 4: Dep = 2.47, *Hiatus = 1.89, Max = 1 (fixed rather than estimated).

Equations

• Storme2026.classicalW = ![2.47, 1.89, 1]

noncomputable def Storme2026.homophonyWeight : ℝ

Fitted weight (posterior mean) of *Homophony: 2.27.

Equations

• Storme2026.homophonyWeight = 2.27

def Storme2026.starHomophony : SystemicConstraint 2 Resolution

*Homophony over the paradigm: collisions among the surface forms of the fixed base (the bare stem) and the two suffixed inputs, via the generic homophonyAvoidance. Homophony is string identity — nothing is stipulated about which outputs collide.

Equations

• Storme2026.starHomophony f = Storme2026.homophonyAvoidance (Matrix.vecCons Storme2026.stem fun (k : Fin 2) => Storme2026.resolve (f k) (Storme2026.inputs k))

*Homophony decomposes over this paradigm

def Storme2026.baseCollisions (j : Phonology.Hiatus.Juncture) (o : Resolution) : ℕ

Collisions between one realized output and its juncture's own bare stem.

Equations

• Storme2026.baseCollisions j o = Storme2026.homophonyAvoidance ![j.stem, Storme2026.resolve o j]

theorem Storme2026.baseCollisions_eq (j : Phonology.Hiatus.Juncture) (o : Resolution) : baseCollisions j o = if o = Resolution.deletion ∧ j.suffixBody = [] then 1 else 0

Only deletion at a monosegmental juncture collides with the base — for any juncture, by the string algebra (Hiatus.Juncture.elideV2_eq_stem_iff and the length facts).

theorem Storme2026.starHomophony_eq_sum (f : Fin 2 → Resolution) : starHomophony f = ∑ k : Fin 2, baseCollisions (inputs k) (f k)

Suffixed outputs never collide with one another, so *Homophony reduces to the per-input base collisions. This is the formal content of [Sto26b]'s fn. 1: on these data, an analysis with a per-mapping constraint against null suffix realization — [AJ21]'s — coincides with the systemic one.

Marginalized mapping probabilities

noncomputable def Storme2026.persianMarginal (k : Fin 2) (o : Resolution) : ℝ

Marginal probability that input k is realized as o — [Sto26b]'s key marginalization equation instantiated to the Persian paradigm.

Equations

• Storme2026.persianMarginal k o = Storme2026.marginalProb Storme2026.inputs Storme2026.classicalCon Storme2026.classicalW ![Storme2026.homophonyWeight] ![Storme2026.starHomophony] k o

noncomputable def Storme2026.foldedScore (j : Phonology.Hiatus.Juncture) (o : Resolution) : ℝ

Per-input harmony with the base-collision penalty folded in.

Equations

• Storme2026.foldedScore j o = Constraints.harmonyScore Storme2026.classicalCon Storme2026.classicalW (j, o) - Storme2026.homophonyWeight * ↑(Storme2026.baseCollisions j o)

theorem Storme2026.foldedScore_eq (k : Fin 2) (o : Resolution) : foldedScore (inputs k) o = -match o with | Resolution.hiatus => 1.89 | Resolution.epenthesis => 2.47 | Resolution.deletion => if k = 0 then 3.27 else 1

Closed form of the folded scores: each candidate's fitted cost, with the *Homophony penalty (2.27, on top of Max's 1) landing exactly on deletion at the monosegmental juncture.

noncomputable def Storme2026.persianUncoupled : CoupledSoftmax (Fin 2) Resolution

The uncoupled equivalent of the Persian model: by starHomophony_eq_sum the coupling folds into the per-input scores.

Equations

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

theorem Storme2026.totalScore_eq (f : Fin 2 → Resolution) : (maxEntCoupled inputs classicalCon classicalW ![homophonyWeight] ![starHomophony]).totalScore f = persianUncoupled.totalScore f

The joint score of the Persian model agrees with its uncoupled equivalent's on every output tuple.

theorem Storme2026.persianMarginal_eq_softmax (k : Fin 2) (o : Resolution) : persianMarginal k o = softmax (foldedScore (inputs k)) o

Closed form for the marginals: the coupling decomposes across positions (starHomophony_eq_sum), so the joint factorizes and each marginal is the softmax of its folded score.

theorem Storme2026.persianMarginal_sum_eq_one (k : Fin 2) : ∑ o : Resolution, persianMarginal k o = 1

The marginals form a probability distribution over the three resolutions.

Predictions with the fitted weights

Table 5's preference orders: hiatus .55 ≻ epenthesis .31 ≻ deletion .14 under the monosegmental suffix, deletion .61 ≻ hiatus .25 ≻ epenthesis .14 under the polysegmental one.

theorem Storme2026.persianMarginal_lt_of_foldedScore_lt {k : Fin 2} {o o' : Resolution} (h : foldedScore (inputs k) o < foldedScore (inputs k) o') : persianMarginal k o < persianMarginal k o'

A marginal comparison reduces to comparing folded scores.

theorem Storme2026.mono_deletion_lt_epenthesis : persianMarginal 0 Resolution.deletion < persianMarginal 0 Resolution.epenthesis

Monosegmental suffix: deletion — which would merge the suffixed form with the bare stem — is the least likely realization (.14).

theorem Storme2026.mono_epenthesis_lt_hiatus : persianMarginal 0 Resolution.epenthesis < persianMarginal 0 Resolution.hiatus

Monosegmental suffix: faithful hiatus is the preferred realization (.55).

theorem Storme2026.poly_epenthesis_lt_hiatus : persianMarginal 1 Resolution.epenthesis < persianMarginal 1 Resolution.hiatus

Polysegmental suffix: epenthesis is less likely than faithful hiatus (.14 vs .25).

theorem Storme2026.poly_hiatus_lt_deletion : persianMarginal 1 Resolution.hiatus < persianMarginal 1 Resolution.deletion

Polysegmental suffix: deletion is the preferred realization (.61) — [hutʃɑmun] keeps the suffix recoverable, so *Homophony is silent.

The suffix-length effect

theorem Storme2026.harmonyScore_inputs_eq (w : Fin 3 → ℝ) (k k' : Fin 2) (o : Resolution) : Constraints.harmonyScore classicalCon w (inputs k, o) = Constraints.harmonyScore classicalCon w (inputs k', o)

The two junctures have identical classical constraint profiles: the classical grammar cannot see the suffix-length difference.

theorem Storme2026.classical_no_length_effect (w : Fin 3 → ℝ) (k k' : Fin 2) (o : Resolution) : marginalProb inputs classicalCon w ![0] ![starHomophony] k o = marginalProb inputs classicalCon w ![0] ![starHomophony] k' o

Without *Homophony the model cannot express a suffix-length effect: for any classical weights the two suffixes receive identical distributions. The qualitative core of [Sto26b]'s model comparison — the fit without *Homophony is worse because classical constraints cannot separate the suffixes at all.

theorem Storme2026.homophony_length_effect : persianMarginal 0 Resolution.deletion < persianMarginal 1 Resolution.deletion

With *Homophony at its fitted weight, deletion is strictly less probable for the monosegmental suffix (predicted frequency .14) than for the polysegmental one (.61): the suffix-length effect of [AJ21].