Harmonic Serialism

[McC00] [McC10] [Pru23] [Lam22c] [Lam22d]

Harmonic Serialism: iterate a one-step gen and a durable constraint ranking to a fixed point. HSDerivation bundles the two; the serial search itself is iterateGen, Function.iterate of a one-round map hsStep on Option C whose fixed points are exactly convergence and failure — durability of both is mathlib's IsFixedPt.iterate; the Nat fuel and the pick tie-breaker make a possibly-non-terminating, possibly-tied search total and computable. One-step EVAL reuses the parallel Tableau machinery; directional EVAL ([Lam22d]; [Eis00]) needs nothing extra — a directional constraint like *FLOAT^→ is a position-indexed scalar block (Tone.starFloatBlock) spliced into the ranking under the canonical lex order.

Main definitions

• hsStep / iterateGen: one total round of the search (convergence and failure are its fixed points), and its n-fold Function.iterate.
• HSDerivation: a one-step gen with a durable ranking; stepOptimum is one GEN/EVAL round, Converged the halting condition, derive the bundled search.

Main results

• iterateGen_eventually_constant: under a well-founded harmony order that every genuine step descends, the search is eventually constant — derivations cannot loop while each step makes measurable progress, so the fuel bound is harmless.
• isFixedPt_singleton_iff_converged: Converged is Function.IsFixedPt of the powerset step at the singleton.
• converged_of_singleton_gen: GEN-restriction to the faithful candidate forces convergence.

Theoretical scope

Per [Pru23] (Table 1), HS does not solve counterfeeding underapplication and only patches counterbleeding with extra GEN assumptions; this file makes no "serial OT solves opacity" claim. [McPL26] is the motivating positive case for the directional variant. Architecturally distinct alternatives in linglib: Phonology/Subregular/LocalRewrite.lean (extrinsic rule ordering) and Phonology/OptimalityTheory/Stratal.lean (cyclic ranking). HS and Stratal OT are sister specializations of parallel OT, not nested: HS holds the ranking constant and iterates the candidate; Stratal OT varies the ranking and chains the candidate (Stratal HS, combining both axes, is deferred — cf. [Pru23] §2.4).

The serial search

def OptimalityTheory.hsStep {C : Type u_1} [DecidableEq C] (step : C → Finset C) (pick : Finset C → Option C) (oc : Option C) : Option C

One total round of the serial search: a converged form (step c = {c}) returns itself, any other advances by picking from the step's output (a canonical sort + head?, or a directional tie-breaker), and failure — an empty pick, or an already failed search — is none. Convergence and failure are both fixed points, so the n-round search is literally Function.iterate of this map.

Equations

• OptimalityTheory.hsStep step pick oc = oc.bind fun (c : C) => if step c = {c} then some c else pick (step c)

def OptimalityTheory.iterateGen {C : Type u_1} [DecidableEq C] (step : C → Finset C) (pick : Finset C → Option C) (n : ℕ) (c : C) : Option C

The n-round search from c: iterate hsStep. The Nat fuel makes the search total — HS need not converge ([Lam22d]).

Equations

• OptimalityTheory.iterateGen step pick n c = (OptimalityTheory.hsStep step pick)^[n] (some c)

@[simp]

theorem OptimalityTheory.hsStep_none {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} : hsStep step pick none = none

@[simp]

theorem OptimalityTheory.hsStep_some {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {c : C} : hsStep step pick (some c) = if step c = {c} then some c else pick (step c)

@[simp]

theorem OptimalityTheory.iterateGen_zero {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {c : C} : iterateGen step pick 0 c = some c

theorem OptimalityTheory.isFixedPt_hsStep_of_converged {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {c : C} (h : step c = {c}) : Function.IsFixedPt (hsStep step pick) (some c)

A converged form is a fixed point of the search step.

theorem OptimalityTheory.isFixedPt_hsStep_none {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} : Function.IsFixedPt (hsStep step pick) none

Failure is a fixed point of the search step.

theorem OptimalityTheory.iterateGen_const_of_converged {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {c : C} (n : ℕ) (h : step c = {c}) : iterateGen step pick n c = some c

At a converged form the search is constant: convergence is durable.

theorem OptimalityTheory.iterateGen_succ_of_step {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {c c' : C} (n : ℕ) (hcv : step c ≠ {c}) (hpick : pick (step c) = some c') : iterateGen step pick (n + 1) c = iterateGen step pick n c'

One round from a non-converged form recurses with the picked successor.

theorem OptimalityTheory.iterateGen_of_pickFail {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {c : C} (n : ℕ) (hcv : step c ≠ {c}) (hpick : pick (step c) = none) : iterateGen step pick (n + 1) c = none

One round from a non-converged form where pick fails yields none, durably.

theorem OptimalityTheory.iterateGen_eventually_constant {C : Type u_1} [DecidableEq C] {step : C → Finset C} {pick : Finset C → Option C} {lt : C → C → Prop} (wf : WellFounded lt) (sound : ∀ (c c' : C), step c ≠ {c} → pick (step c) = some c' → c' ≠ c → lt c' c) (c : C) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → iterateGen step pick m c = iterateGen step pick N c

HS terminates under a well-founded harmony order. If every genuine step descends a well-founded lt (sound), the search is eventually constant: some N past which further fuel doesn't change the result. Derivations cannot loop while each step makes measurable progress, so the explicit Nat bound is harmless. The proof is WellFounded.iterate_eventually_constant over the harmony order lifted to Option.

HS derivations

structure OptimalityTheory.HSDerivation (C : Type u_1) [DecidableEq C] : Type u_1

A Harmonic Serialism derivation: a one-step candidate-generation function (per [McC08]'s restricted GEN) and a durable ranking. The inner Tableau width is ranking.length.

• gen : C → Finset C

  The one-step candidate-generation function.

• ranking : List (Constraints.Constraint C)

  The constraint ranking, durable across rounds (head = highest).

def OptimalityTheory.HSDerivation.tableauFor {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (cands : Finset C) (h : cands.Nonempty) : Tableau C D.ranking.length

The inner tableau on an explicit nonempty candidate set, scored by D.ranking.

Equations

• D.tableauFor cands h = { candidates := cands, profile := Constraints.buildViolationProfile D.ranking.get, nonempty := h }

@[simp]

theorem OptimalityTheory.HSDerivation.tableauFor_profile {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (cands : Finset C) (h : cands.Nonempty) : (D.tableauFor cands h).profile = Constraints.buildViolationProfile D.ranking.get

def OptimalityTheory.HSDerivation.evalFilter {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (cands : Finset C) : Finset C

Filter a candidate set to its optimal subset under D.ranking; ∅ on empty input. This is the one-step EVAL of the serial search.

Equations

• D.evalFilter cands = if h : cands.Nonempty then (D.tableauFor cands h).optimal else ∅

def OptimalityTheory.HSDerivation.stepOptimum {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : Finset C

The optimal set of one GEN/EVAL round.

Equations

• D.stepOptimum c = D.evalFilter (D.gen c)

@[simp]

theorem OptimalityTheory.HSDerivation.stepOptimum_of_empty_gen {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) (h : D.gen c = ∅) : D.stepOptimum c = ∅

An empty gen output yields an empty optimal set.

Convergence

def OptimalityTheory.HSDerivation.Converged {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : Prop

A form has converged iff its one-round optimal set is the singleton of the faithful candidate — the canonical HS halting condition ([McC10]).

Equations

• D.Converged c = (D.stepOptimum c = {c})

@[implicit_reducible]

instance OptimalityTheory.HSDerivation.instDecidableConverged {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : Decidable (D.Converged c)

Equations

• D.instDecidableConverged c = decEq (D.stepOptimum c) {c}

@[simp]

theorem OptimalityTheory.HSDerivation.isFixedPt_singleton_iff_converged {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : Function.IsFixedPt (fun (s : Finset C) => s.biUnion D.stepOptimum) {c} ↔ D.Converged c

Converged is Function.IsFixedPt of the powerset step s ↦ ⋃ x ∈ s, stepOptimum x at the singleton {c} — by Finset.singleton_biUnion, with no intermediate combinator. Simp-normalized toward Converged.

theorem OptimalityTheory.HSDerivation.converged_of_singleton_gen {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) (h : D.gen c = {c}) : D.Converged c

GEN-restriction to the faithful candidate forces convergence.

def OptimalityTheory.HSDerivation.derive {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) (pick : Finset C → Option C) (steps : ℕ) : Option C

An n-round HS derivation: iterateGen over stepOptimum with a caller-supplied pick tie-breaker for non-singleton optima (ties not yet broken by directional eval, or genuinely divergent ties in the [Pru09] sense).

Equations

• D.derive c pick steps = OptimalityTheory.iterateGen D.stepOptimum pick steps c