Yolyan 2025: Weak Determinism as Simultaneous Application

[Yol25]: weakly deterministic functions are those expressible as the simultaneous application P^L ⊙ P^R of a backward and a forward BMRS program (Def. 5.1) — a definition inside the program formalism, which for the first time makes non-membership provable. IsBmrsWeaklyDeterministic renders it via the value-level ⊙ of Logic/BMRS.lean: SimulModels asks each output symbol to be the ⊙-combination of the two programs' output predicates against the input (Defs. 4.1/4.3), sparing the combined-head-space construction.

The engine is not_isBmrsWeaklyDeterministic_of_requiresBothSides: the paper's §5.3 template (Thms. 5.2–5.5), consuming the same Subregular.RequiresBothSides witness that excludes the bimachine rendering of weak determinism (not_isBimachineWeaklyDeterministic_of_requiresBothSides). Whether the two definitions coincide is the paper's own open question (§6.3, against [MMBMcC24]); feeding both exclusions one witness object states it structurally without resolving it. The proof here streamlines the paper's: on either perturbation the input value is unchanged, so ⊙ collapses to conjunction and both one-sided outputs are forced true; each transports to the base word by one-sided locality (Eval.congr_agreeUpto/congr_agreeFrom), and recombining forces the base unchanged — no case-split through Prop. 4.2 needed. Only the d = 0 instance of the witness is used: one-sidedness is global, not window-bounded.

Instances: Sour Grapes harmony (Thm. 5.2 — the first proof of the [HL13] conjecture, via [Pad95]/[Wil03b]'s pathology), and — through the shared witnesses already in the library — Tutrugbu ATR harmony (Prop. 5.5, [McCBMM20]), Luganda unbounded tonal plateauing ([Jar16]), and Copperbelt Bemba high-tone spreading (Prop. 5.4), the latter formalized here as a second Tone.Surfacing instance. The positive side: with no underlying stress the input predicate is constantly ⊥ and ⊙ collapses to disjunction — (5.15), recovering [KJ20]'s LHOL program as the simultaneous application of its two one-sided halves. §6.3's conjunctive dual ⊘ is exact on Sour Grapes: sourGrapes_conjunctive shows the map is the ⊘ of its one-sided licensing conditions.

Weak determinism as simultaneous application (Defs. 4.1, 4.3, 5.1)

def Yolyan2025.SimulEval {α : Type u_1} [DecidableEq α] {L R : Type} (PL : Subregular.Logic.BMRS.Program α L) (PR : Subregular.Logic.BMRS.Program α R) (hL : L) (hR : R) (w : Subregular.Logic.WordModel α) (i : ℕ) (σ : α) (b : Bool) : Prop

The value of the ⊙-combined output predicate for σ at i ([Yol25] Def. 4.1): the two programs' output values combined against the input value.

Equations

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

def Yolyan2025.SimulModels {α : Type u_1} [DecidableEq α] {L R : Type} (PL : Subregular.Logic.BMRS.Program α L) (PR : Subregular.Logic.BMRS.Program α R) (outL : α → L) (outR : α → R) (f : List α → List α) : Prop

The simultaneous application P^L ⊙ P^R models f (Def. 4.3, restricted to the length-preserving maps of §5): each output symbol is the one whose ⊙-combined output predicate holds.

Equations

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

def Yolyan2025.IsBmrsWeaklyDeterministic {α : Type u_1} [DecidableEq α] (f : List α → List α) : Prop

Def. 5.1: f is weakly deterministic when it is the simultaneous application of a backward (BMRSᵖ) and a forward (BMRSˢ) program. Head types are unconstrained (the paper's are finite), which only strengthens the negative results below.

Equations

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

The exclusion template (§5.3)

theorem Yolyan2025.not_isBmrsWeaklyDeterministic_of_requiresBothSides {α : Type u_1} [DecidableEq α] {f : List α → List α} (hf : Subregular.RequiresBothSides f) : ¬IsBmrsWeaklyDeterministic f

The §5.3 template, proven once: a map that requires both sides is not weakly deterministic. On the far-left perturbation the target is unchanged, so ⊙ is conjunction and both one-sided outputs are true; the forward one transports to the base by locality. Symmetrically the far-right perturbation delivers the backward one. Recombining in the base forces the target unchanged — contradiction. Thms. 5.2, 5.3 and Props. 5.4, 5.5 are instances.

Sour Grapes harmony is not weakly deterministic (Thm. 5.2)

The pathology of [Pad95]/[Wil03b]: − becomes + iff a + lies anywhere to its left and no blocker ⊟ anywhere to its right — spreading happens only when it can reach the end of the word.

inductive Yolyan2025.SG : Type

The schematic Sour Grapes alphabet: trigger +, target −, blocker ⊟.

• plus : SG
• minus : SG
• blk : SG

@[implicit_reducible]

instance Yolyan2025.instDecidableEqSG : DecidableEq SG

Equations

• Yolyan2025.instDecidableEqSG x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Yolyan2025.instReprSG : Repr SG

Equations

• Yolyan2025.instReprSG = { reprPrec := Yolyan2025.instReprSG.repr }

def Yolyan2025.instReprSG.repr : SG → ℕ → Std.Format

Equations

• Yolyan2025.instReprSG.repr Yolyan2025.SG.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.SG.plus")).group prec✝
• Yolyan2025.instReprSG.repr Yolyan2025.SG.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.SG.minus")).group prec✝
• Yolyan2025.instReprSG.repr Yolyan2025.SG.blk prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.SG.blk")).group prec✝

def Yolyan2025.sourGrapes (w : List SG) : List SG

Sour Grapes harmony, by the paper's own characterization: a − surfaces + iff a trigger precedes it and no blocker follows it.

Equations

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

theorem Yolyan2025.sourGrapes_requiresBothSides : Subregular.RequiresBothSides sourGrapes

Sour Grapes requires both sides: the middle of + −…− − spreads, but neither the triggerless − −…− − (far-left perturbation) nor the blocked + −…− ⊟ (far-right) changes it.

theorem Yolyan2025.sourGrapes_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic sourGrapes

Thm. 5.2 — the first proof of the [HL13] conjecture.

theorem Yolyan2025.sourGrapes_not_bimachineWeaklyDeterministic : ¬Subregular.IsBimachineWeaklyDeterministic sourGrapes

The same witness excludes the bimachine rendering of weak determinism — the two exclusions consume one object, which is the sharpest formal statement available of the paper's §6.3 open question (are the two definitions equivalent?).

The library's unbounded-circumambient maps, through the same template

theorem Yolyan2025.tutrugbu_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic McCollumEtAl2020.tutrugbuATR

Prop. 5.5 (Tutrugbu ATR harmony is not weakly deterministic), riding the witness already formalized for the bimachine side in Studies/McCollumEtAl2020.

theorem Yolyan2025.utp_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic Tone.Plateauing.utp.map

Luganda unbounded tonal plateauing is not weakly deterministic: [Jar16]'s flagship pattern (the class of the paper's Prop. 5.4 Bemba case), through Phonology/Tone/Plateauing's witness.

Bemba high-tone spreading is not weakly deterministic (Prop. 5.4)

Copperbelt Bemba ([Jar16]; the paper's bounded/unbounded spreading data): a high tone spreads to the end of the word when no high follows it, and only onto the next two TBUs when one does. A second Tone.Surfacing instance — and a cautionary one: unlike plateauing, the surface set is not convex and the map is neither monotone nor idempotent, so only the shared surfacing API transfers.

inductive Yolyan2025.BTone : Type

The Bemba tonal alphabet.

• H : BTone
• L : BTone

@[implicit_reducible]

instance Yolyan2025.instDecidableEqBTone : DecidableEq BTone

Equations

• Yolyan2025.instDecidableEqBTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yolyan2025.instReprBTone.repr : BTone → ℕ → Std.Format

Equations

• Yolyan2025.instReprBTone.repr Yolyan2025.BTone.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.BTone.H")).group prec✝
• Yolyan2025.instReprBTone.repr Yolyan2025.BTone.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.BTone.L")).group prec✝

@[implicit_reducible]

instance Yolyan2025.instReprBTone : Repr BTone

Equations

• Yolyan2025.instReprBTone = { reprPrec := Yolyan2025.instReprBTone.repr }

def Yolyan2025.bembaSurfaces (w : List BTone) (i : ℕ) : Prop

Position i surfaces H: an underlying H, within the two-TBU bounded spread of a preceding H, or at-or-after the last H (unbounded spread to the word end).

Equations

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

@[implicit_reducible]

instance Yolyan2025.instDecidableBembaSurfaces (w : List BTone) (i : ℕ) : Decidable (bembaSurfaces w i)

Equations

• Yolyan2025.instDecidableBembaSurfaces w i = id inferInstance

def Yolyan2025.bemba : Tone.Surfacing BTone

Bemba high-tone spreading as a surfacing process.

Equations

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

theorem Yolyan2025.bemba_requiresBothSides : Subregular.RequiresBothSides bemba.map

Bemba spreading requires both sides: the middle of H L…L L spreads (unbounded, no blocker), but neither the triggerless far-left flip nor the far-right H (which bounds the spread to two TBUs) changes it.

theorem Yolyan2025.bemba_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic bemba.map

Prop. 5.4: Bemba high-tone spreading is not weakly deterministic.

theorem Yolyan2025.bemba_not_bimachineWeaklyDeterministic : ¬Subregular.IsBimachineWeaklyDeterministic bemba.map

The bimachine twin, off the same witness.

The positive side: LHOL stress as a simultaneous application (§5.2)

Leftmost-heavy-otherwise-leftmost stress ([KJ20]; Lushootseed): stress the leftmost heavy syllable, else the leftmost syllable. The backward program finds a heavy with no heavy to its left; the forward program stresses an initial light with no heavy to its right. No syllable is underlyingly stressed, so the input predicate is constantly ⊥ and ⊙ collapses to disjunction — (5.15), the Koser–Jardine program.

inductive Yolyan2025.Syll : Type

Syllable weight.

• H : Syll
• L : Syll

@[implicit_reducible]

instance Yolyan2025.instDecidableEqSyll : DecidableEq Syll

Equations

• Yolyan2025.instDecidableEqSyll x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yolyan2025.instReprSyll.repr : Syll → ℕ → Std.Format

Equations

• Yolyan2025.instReprSyll.repr Yolyan2025.Syll.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.Syll.H")).group prec✝
• Yolyan2025.instReprSyll.repr Yolyan2025.Syll.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.Syll.L")).group prec✝

@[implicit_reducible]

instance Yolyan2025.instReprSyll : Repr Syll

Equations

• Yolyan2025.instReprSyll = { reprPrec := Yolyan2025.instReprSyll.repr }

inductive Yolyan2025.LHead : Type

Heads of the backward stress program: noHL = no heavy anywhere left (5.8).

• noHL : LHead
• stressL : LHead

@[implicit_reducible]

instance Yolyan2025.instDecidableEqLHead : DecidableEq LHead

Equations

• Yolyan2025.instDecidableEqLHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Yolyan2025.RHead : Type

Heads of the forward stress program: noHR = no heavy anywhere right (5.9).

• noHR : RHead
• stressR : RHead

@[implicit_reducible]

instance Yolyan2025.instDecidableEqRHead : DecidableEq RHead

Equations

• Yolyan2025.instDecidableEqRHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yolyan2025.lholL : Subregular.Logic.BMRS.Program Syll LHead

(5.8), (5.12): stress a heavy with no heavy to its left.

Equations

• One or more equations did not get rendered due to their size.
• Yolyan2025.lholL Yolyan2025.LHead.stressL = (Subregular.Logic.BMRS.Expr.label {Yolyan2025.Syll.H} Yolyan2025.x✝).and (Subregular.Logic.BMRS.Expr.call Yolyan2025.LHead.noHL Yolyan2025.x✝)

def Yolyan2025.lholR : Subregular.Logic.BMRS.Program Syll RHead

(5.9), (5.11): stress an initial light with no heavy to its right.

Equations

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

theorem Yolyan2025.lholL_backward : lholL.Backward

theorem Yolyan2025.lholR_forward : lholR.Forward

theorem Yolyan2025.lhol_LHLLH : List.map (fun (i : ℕ) => (Subregular.Logic.BMRS.evalFuel lholL [Syll.L, Syll.H, Syll.L, Syll.L, Syll.H] 32 i (Subregular.Logic.BMRS.Expr.call LHead.stressL Yolyan2025.x✝)).bind fun (bL : Bool) => Option.map (fun (bR : Bool) => Subregular.Logic.BMRS.combine false bL bR) (Subregular.Logic.BMRS.evalFuel lholR [Syll.L, Syll.H, Syll.L, Syll.L, Syll.H] 32 i (Subregular.Logic.BMRS.Expr.call RHead.stressR Yolyan2025.x✝))) (List.range 5) = [some false, some true, some false, some false, some false]

With no underlying stress, ⊙ is the disjunction of the two programs — (5.15). On LHLLH the backward program stresses the leftmost heavy alone.

theorem Yolyan2025.lhol_LLLL : List.map (fun (i : ℕ) => (Subregular.Logic.BMRS.evalFuel lholL [Syll.L, Syll.L, Syll.L, Syll.L] 32 i (Subregular.Logic.BMRS.Expr.call LHead.stressL Yolyan2025.x✝)).bind fun (bL : Bool) => Option.map (fun (bR : Bool) => Subregular.Logic.BMRS.combine false bL bR) (Subregular.Logic.BMRS.evalFuel lholR [Syll.L, Syll.L, Syll.L, Syll.L] 32 i (Subregular.Logic.BMRS.Expr.call RHead.stressR Yolyan2025.x✝))) (List.range 4) = [some true, some false, some false, some false]

On all-light LLLL the forward program stresses the initial syllable alone.

§6.3: Sour Grapes is conjunctively simultaneous

theorem Yolyan2025.sourGrapes_conjunctive {w : List SG} {i : ℕ} (hm : w[i]? = some SG.minus) : (sourGrapes w)[i]? = some (if Subregular.Logic.BMRS.combineC false (decide (SG.plus ∈ List.take i w)) (decide (SG.blk ∉ List.drop i w)) = true then SG.plus else SG.minus)

Sour Grapes is the conjunctive simultaneous application ⊘ (Def. 6.5) of its two one-sided licensing conditions: at a target, spreading happens iff the backward condition (a trigger left) and the forward condition (no blocker right) both fire. The disjunctive ⊙ cannot express this (Thm. 5.2); ⊘ does so exactly — the paper's §6.3 route toward characterizing unbounded circumambience.