Harmonic Serialism — The Combinator

@cite{mccarthy-2000} @cite{mccarthy-2010} @cite{pruitt-2023} @cite{lamont-2022a} @cite{lamont-2022b}

Bundles a one-step gen function and a constraint ranking into an HSDerivation. Reuses the iteration combinator from Iteration.lean and the existing parallel Tableau/mkTableau machinery from Basic.lean (Layered Grounding — does not duplicate parallel optimization).

NOTE on theoretical scope

Per @cite{pruitt-2023} (Table 1): HS does not solve counterfeeding underapplication, and only patches counterbleeding overapplication with extra GEN assumptions. This file's docstring deliberately does not claim HS is "the serial OT solution to opacity" — that would misrepresent the field's current understanding. HS is one constraint-based serial framework with mixed empirical record; @cite{mcpherson-lamont-2026} is the motivating positive case for the directional variant of HS (@cite{lamont-2022b}). For counterfeeding cases linglib offers Theories/Phonology/Process/LocalRewrite.lean (extrinsic ordering of local rewrite rules; subregular-grounded per @cite{chandlee-heinz-2018}) and Theories/Phonology/OptimalityTheory/Stratal.lean (cyclic ranking) as architecturally-distinct alternatives.

Sibling architectures

OT has multiple "more than one EVAL call" specializations, all sharing the parallel-OT primitives in Basic.lean:

Theory	Ranking across calls	Candidate across calls
Parallel OT (Basic.lean)	n/a (single call)	n/a
Stratal OT (Stratal.lean)	varies per stratum	chained via bridge
HS (this file)	durable	iterated via gen
Stratal HS (not yet)	varies per stratum	iterated within stratum

HS and Stratal OT are sister specializations, not nested: HS holds ranking constant and varies the candidate; Stratal OT varies the ranking and chains the candidate. Stratal HS combines both axes and is deferred (cf. @cite{pruitt-2023} §2.4).

Sibling, not refactor

This module does not modify NamedConstraint or Tableau (load-bearing for Weighted.lean/MaxEnt.lean/NoisyHG.lean and ~30 study files). The stepOptimum function builds an inner Tableau and reuses Tableau.optimal directly. Future directional dispatch (@cite{lamont-2022b}; @cite{eisner-2000}) will land as a sibling DirectionalTableau consumer; deliberately not stubbed here, to avoid silently routing directional callers to the parallel optimum.

structure Core.Constraint.OT.HSDerivation (C : Type u_1) [DecidableEq C] : Type u_1

A Harmonic Serialism derivation specification.

gen is the one-step candidate-generation function (per @cite{mccarthy-2008b}'s restricted GEN). ranking is a list of named constraints, indexed by rank position (head = highest). The inner Tableau width is inferred from ranking.length; no separate length parameter is exposed.

• gen : C → Finset C
• ranking : List (NamedConstraint C)

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

Build a Tableau from an explicit candidate set, given D.ranking. Defined when the candidate set is non-empty. Reuses mkProfile (Layered Grounding — does not duplicate the buildViolationProfile body).

Equations

• D.tableauFor cands h = { candidates := cands, profile := Core.Constraint.OT.mkProfile D.ranking, nonempty := h }

@[simp]

theorem Core.Constraint.OT.HSDerivation.tableauFor_profile {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (cands : Finset C) (h : cands.Nonempty) : (D.tableauFor cands h).profile = mkProfile D.ranking

The inner tableau's profile is exactly mkProfile D.ranking.

def Core.Constraint.OT.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. Returns ∅ on empty input. Routes through the existing parallel Tableau.optimal (Layered Grounding — does not duplicate parallel optimization). This is the eval : Finset C → Finset C consumed by Iteration.iterateGen.

Equations

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

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

Optimal set for one HS step: evalFilter applied to gen c. Equivalently, Iteration.iterateStep D.gen D.evalFilter c.

Equations

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

@[simp]

theorem Core.Constraint.OT.HSDerivation.stepOptimum_eq_iterateStep {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : D.stepOptimum c = iterateStep D.gen D.evalFilter c

@[simp]

theorem Core.Constraint.OT.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.

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

A form c has converged under D iff its optimal set is the singleton {c} — the faithful candidate is the unique optimum. This is the canonical HS halting condition (@cite{mccarthy-2010}).

Equivalent to mathlib's Function.IsFixedPt (hsStep D.gen D.evalFilter) {c} via hsStep_singleton.

Equations

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

@[implicit_reducible]

instance Core.Constraint.OT.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 Core.Constraint.OT.HSDerivation.isFixedPt_hsStep_singleton_iff_converged {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : Function.IsFixedPt (hsStep D.gen D.evalFilter) {c} ↔ D.Converged c

Converged is exactly mathlib's Function.IsFixedPt applied to the powerset-lifted step at the singleton input. The bridge direction is IsFixedPt → Converged (more complex → simpler), so the simp lemma is registered in that direction.

theorem Core.Constraint.OT.HSDerivation.converged_iff_isFixedPt {C : Type u_1} [DecidableEq C] (D : HSDerivation C) (c : C) : D.Converged c ↔ Function.IsFixedPt (hsStep D.gen D.evalFilter) {c}

Convenience flip of isFixedPt_hsStep_singleton_iff_converged. Not a simp lemma in this direction — would rewrite the simpler Converged form to the more complex IsFixedPt form.

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

Sufficient condition for convergence: when gen produces only the faithful candidate, the form is converged. This is the structural soundness statement that GEN-restriction at a candidate forces the HS halting condition.

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

n-step HS derivation. Wraps iterateGen with D.gen and D.stepOptimum. The caller supplies a pick : Finset C → Option C tie-breaker used when the optimal set isn't a singleton (which would indicate either (a) ties not yet broken by directional eval, or (b) a divergent tie in the @cite{pruitt-2009} sense). Returns none if pick ever fails. HS derivations are not in general guaranteed to converge — see @cite{lamont-2022b} for non-terminating cases.

Equations

• D.derive pick c steps = Core.Constraint.OT.iterateGen D.gen D.evalFilter pick c steps

def Core.Constraint.OT.pickByOrder {C : Type u_1} [LinearOrder C] (s : Finset C) : Option C

Canonical tie-breaker for HSDerivation.derive when C carries a LinearOrder: pick the order-minimal element of the optimal set. The ordering is typically incidental (a paper-grounded LinearOrder.lift' through a toNat injection) since vanilla HS doesn't specify how to break ties; directional HS replaces this with EvalMode.directional once the DirectionalTableau consumer arrives. Promoted out of the HSDerivation namespace because it operates on bare Finset C and is reusable wherever an HS-style iteration needs a canonical tie-breaker.

Equations

• Core.Constraint.OT.pickByOrder s = if h : s.Nonempty then some (s.min' h) else none

inductive Core.Constraint.OT.HSDerivation.Toy : Type

Two-character toy alphabet for the substrate's smoke test.

• a : Toy
• b : Toy

@[implicit_reducible]

instance Core.Constraint.OT.HSDerivation.instDecidableEqToy : DecidableEq Toy

Equations

• Core.Constraint.OT.HSDerivation.instDecidableEqToy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Constraint.OT.HSDerivation.instReprToy.repr : Toy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Constraint.OT.HSDerivation.instReprToy : Repr Toy

Equations

• Core.Constraint.OT.HSDerivation.instReprToy = { reprPrec := Core.Constraint.OT.HSDerivation.instReprToy.repr }

def Core.Constraint.OT.HSDerivation.toyGen : Toy → Finset Toy

Toy GEN: every form admits only itself. This makes every form a fixed point of every HSDerivation built over Toy (no harmonic improvement is possible). The smoke test exercises the convergence machinery on the trivial-GEN case.

Equations

• Core.Constraint.OT.HSDerivation.toyGen c = {c}

def Core.Constraint.OT.HSDerivation.toyRanking : List (NamedConstraint Toy)

Toy ranking: a single faithfulness constraint that is satisfied by every candidate (returns 0 always). Evaluation is then trivially parallel.

Equations

• Core.Constraint.OT.HSDerivation.toyRanking = [{ name := "TOY-FAITH", family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := fun (x : Core.Constraint.OT.HSDerivation.Toy) => 0 }]

def Core.Constraint.OT.HSDerivation.toyDerivation : HSDerivation Toy

The toy HSDerivation.

Equations

• Core.Constraint.OT.HSDerivation.toyDerivation = { gen := Core.Constraint.OT.HSDerivation.toyGen, ranking := Core.Constraint.OT.HSDerivation.toyRanking }

Directional HS (@cite{lamont-2022b}): the constraint hierarchy is a list of DirectionalConstraint C, evaluated via DirectionalTableau under a chosen EvalMode. Sibling to the parallel HSDerivation above; the two are not unified because their constraint types differ (NamedConstraint C for parallel vs DirectionalConstraint C for directional) and weighted aggregation is theoretically incoherent with directional EVAL (per Lamont 2022b).

The motivating consumer is paper, fig. 3 (`/kāk^H + rī^H + dō^H/`):
parallel HS produces a divergent tie among three deletion candidates;
directional `*FLOAT^→` breaks the tie by requiring leftmost-first
deletion. 

structure Core.Constraint.OT.DirectionalHSDerivation (C : Type u_1) [DecidableEq C] : Type u_1

• gen : C → Finset C
• ranking : List (DirectionalConstraint C)
• evalMode : EvalMode

def Core.Constraint.OT.DirectionalHSDerivation.tableauFor {C : Type u_1} [DecidableEq C] (D : DirectionalHSDerivation C) (cands : Finset C) (h : cands.Nonempty) : DirectionalTableau C

Build a DirectionalTableau from an explicit candidate set.

Equations

• D.tableauFor cands h = { candidates := cands, ranking := D.ranking, evalMode := D.evalMode, nonempty := h }

def Core.Constraint.OT.DirectionalHSDerivation.evalFilter {C : Type u_1} [DecidableEq C] (D : DirectionalHSDerivation C) (cands : Finset C) : Finset C

Filter a candidate set to its optimal subset under D.ranking and D.evalMode. Routes through DirectionalTableau.optimal (Layered Grounding). Returns ∅ on empty input.

Equations

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

def Core.Constraint.OT.DirectionalHSDerivation.stepOptimum {C : Type u_1} [DecidableEq C] (D : DirectionalHSDerivation C) (c : C) : Finset C

Optimal set for one HS step under directional EVAL.

Equations

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

def Core.Constraint.OT.DirectionalHSDerivation.Converged {C : Type u_1} [DecidableEq C] (D : DirectionalHSDerivation C) (c : C) : Prop

A form c has converged under D iff its optimal set under directional EVAL is {c}.

Equations

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

@[implicit_reducible]

instance Core.Constraint.OT.DirectionalHSDerivation.instDecidableConverged {C : Type u_1} [DecidableEq C] (D : DirectionalHSDerivation C) (c : C) : Decidable (D.Converged c)

Equations

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

def Core.Constraint.OT.DirectionalHSDerivation.derive {C : Type u_1} [DecidableEq C] (D : DirectionalHSDerivation C) (pick : Finset C → Option C) (c : C) (steps : ℕ) : Option C

N-step directional HS derivation. Wraps iterateGen with D.gen and D.evalFilter. The caller supplies a pick : Finset C → Option C tie-breaker; under directional EVAL ties should be rare or absent (that's the whole point of using directional), but pick is still needed for the fallback path. The substrate utility pickByOrder (above) suffices when C carries a LinearOrder.

Equations

• D.derive pick c steps = Core.Constraint.OT.iterateGen D.gen D.evalFilter pick c steps