Tier-Based Alternation Rules

@cite{belth-2026} @cite{goldsmith-1976}

The canonical operational schema for SPE-style phonological alternations that factor through a tier projection. A rule has the shape

Rel(A, F) / C __ ∘ proj(·, T) (left-context, eq. 6 of @cite{belth-2026}) Rel(A, F) / __ C ∘ proj(·, T) (right-context, eq. 8)

where:

• T ⊆ α is a tier (an erasing string-homomorphism — see Core.Tier);
• C ⊆ T is the natural class of the triggering tier-adjacent segment;
• A ⊆ α is the natural class of targets (here: a single underspecified position identified by index, à la @cite{belth-2026});
• F is the agreed-or-disagreed feature; and
• Rel is Agree (assimilation) or Disagree (dissimilation).

This schema covers Belth-style D2L rules (Latin -alis / -aris liquid dissimilation, Turkish vowel harmony, Finnish backness harmony with neutral-vowel transparency — see @cite{belth-2026}), Rose-Walker harmony systems (which structurally contain a TierRule as their value-prediction core — see Phonology.Harmony.HarmonySystem in Harmony/Defs.lean), and any SPE rule whose context is a single tier-adjacent segment.

The schema does not cover:

• multi-feature dependencies (e.g., Turkish back/round parasitic harmony) — would require generalising featureValue : α → Option Bool to a list;
• non-local context windows (e.g., "the second segment to the left on the tier") — would require a positional offset on top of lastWith.

Both extensions are admittable on demand following the project's "infrastructure on demand" policy (see CLAUDE.md).

Relation to Process/LocalRewrite.lean

Theories/Phonology/Process/LocalRewrite.lean defines Rule — full SPE notation with arbitrary-length left/right contexts. The single-tier- segment-context fragment of Rules is structurally subsumed by TierRule (via the trivial-tier specialisation theorem id_tier_left_is_strict_local below). The formal subsumption bridge theorem between the two rule types is deferred — it would state that for any LocalRewrite.Rule whose left/right contexts are each a single .seg element, there exists a TierRule computing the same string function. Lean-checkable formulation is straightforward but requires careful threading of the trivial tier; land it once a Studies file needs to invoke the bridge concretely.

inductive Phonology.Alternation.Relation : Type

Belth's Agree/Disagree distinction (@cite{belth-2026} eq. 9).

• agree : Relation
• disagree : Relation

@[implicit_reducible]

instance Phonology.Alternation.instDecidableEqRelation : DecidableEq Relation

Equations

• Phonology.Alternation.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Alternation.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Alternation.instReprRelation : Repr Relation

Equations

• Phonology.Alternation.instReprRelation = { reprPrec := Phonology.Alternation.instReprRelation.repr }

def Phonology.Alternation.Relation.flip : Relation → Relation

The relation flipped: .agree ↔ .disagree.

Equations

• Phonology.Alternation.Relation.agree.flip = Phonology.Alternation.Relation.disagree
• Phonology.Alternation.Relation.disagree.flip = Phonology.Alternation.Relation.agree

@[simp]

theorem Phonology.Alternation.Relation.flip_flip (r : Relation) : r.flip.flip = r

Flipping the relation twice returns the original.

@[reducible, inline]

abbrev Phonology.Alternation.Side : Type

Which side the context lies on relative to the unspecified target slot.

• .left — Rel(A, F) / C __ : context precedes the target
• .right — Rel(A, F) / __ C : context follows the target

Aliased to Core.Direction so the same .left / .right cases used by Function/Subsequential.lean::Direction (FST scan direction) and by this file (context side of a tier rule) reduce to one inductive type. The two roles read differently in prose but are isomorphic in Lean.

Equations

• Phonology.Alternation.Side = Core.Direction

structure Phonology.Alternation.TierRule (α : Type) : Type

A tier-based alternation rule over alphabet α.

• tier : the erasing projection (@cite{goldsmith-1976}) onto which the context-class check is performed.
• side : whether the triggering context precedes (.left, eq. 6) or follows (.right, eq. 8) the unspecified target slot.
• targetIsContext : the natural class C — the rule fires only when the tier-adjacent segment satisfies this predicate. Following mathlib's Finset.filter convention this is Prop-valued with [DecidablePred] carried as the instance field decTarget.
• relation : .agree (assimilation) or .disagree (dissimilation).
• featureValue : the value of F extracted from a context segment. none means the segment is itself underspecified for F, in which case the rule defers to default.
• default : the Elsewhere value (@cite{belth-2026} §2.3.3, Finnish 52b). none means no default — when no context is found, applyAt returns none. some v is the concrete fallback.

• tier : Core.Tier α α
• side : Side
• targetIsContext : α → Prop
• decTarget : DecidablePred self.targetIsContext
• relation : Relation
• featureValue : α → Option Bool
• default : Option Bool

def Phonology.Alternation.TierRule.apply {α : Type} (r : TierRule α) (pre post : List α) : Option Bool

The value the rule predicts at the unspecified slot, given the rule r, the preceding segments pre, and the following segments post. The chosen side (r.side) determines which list is consulted.

Returns none only when there is no relevant context and no default — i.e., the rule has no opinion.

Equations

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

def Phonology.Alternation.TierRule.applyAt {α : Type} (r : TierRule α) (pre : List α) : Option Bool

Convenience for left-context rules: only the preceding string matters. The Belth Latin / Turkish-VH / Finnish-VH rules all use this form.

Equations

• r.applyAt pre = r.apply pre []

def Phonology.Alternation.TierRule.flipRelation {α : Type} (r : TierRule α) : TierRule α

The rule with its relation flipped (Agree ↔ Disagree).

Equations

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

@[simp]

theorem Phonology.Alternation.TierRule.flipRelation_flipRelation {α : Type} (r : TierRule α) : r.flipRelation.flipRelation = r

Flipping the relation twice returns the original rule.

theorem Phonology.Alternation.TierRule.id_tier_left_is_strict_local {α : Type} (r : TierRule α) (h_id : r.tier = Core.Tier.id) (h_side : r.side = Core.Direction.left) (pre : List α) : r.apply pre [] = match (List.filter (fun (x : α) => decide (r.targetIsContext x)) pre).getLast? with | none => r.default | some ctx => match r.featureValue ctx with | none => r.default | some v => some (match r.relation with | Relation.agree => v | Relation.disagree => !v)

Strict locality is the trivial-tier special case. When the tier is the identity (every segment projects), apply (left-context) reduces to scanning the raw input for the context class — i.e., a strictly local rule (@cite{belth-2026} §2.4 example: Turkish voicing assimilation eq. 49b is Agree([?voice], {voice}) / [*] __ with the trivial projection).

def Phonology.Alternation.TierRule.applyToString {α : Type} (r : TierRule α) (input : List α) : List (Option Bool)

Reify a TierRule as a string-to-string function: at each input position, predict the feature value for the implicit "hole" using the preceding context. The result is a List α → List (Option Bool) function that consumers can classify subregularly.

Defined recursively (via applyToStringAux) for ease of induction; the output at position i is applyAt r (input.take i) per the auxiliary's past-threading.

Equations

• r.applyToString input = Phonology.Alternation.TierRule.applyToString.applyToStringAux r input []

def Phonology.Alternation.TierRule.applyToString.applyToStringAux {α : Type} (r : TierRule α) (input past : List α) : List (Option Bool)

Auxiliary: emit predictions over the suffix input, using past as the accumulated past.

Equations

• Phonology.Alternation.TierRule.applyToString.applyToStringAux r [] past = []
• Phonology.Alternation.TierRule.applyToString.applyToStringAux r (x_2 :: xs) past = r.applyAt past :: Phonology.Alternation.TierRule.applyToString.applyToStringAux r xs (past ++ [x_2])

Bridge to function-level subregular substrate

The TierRule.applyToString reification produces a string-to-string function classifiable in the function-level subregular hierarchy (Core/Computability/Subregular/Function/). The expected classification per @cite{aksenova-rawski-graf-heinz-2020}:

• Identity-tier TierRules → Left-Subsequential (the trivial-tier case lemma id_tier_left_is_strict_local above shows the structural equivalence to scanning the raw input for the context class).
• Non-trivial-tier TierRules → Tier-Subsequential (a strictly larger class than Left-Subsequential, captured by the standard Heinz-Rawski-Tanner 2011 tier-strictly-local family applied to function classes).

This bridge theorem is deferred in this PR (substantive new construction; the SFST witness needs to thread the tier projection's state alongside the predicate-evaluation state). The substrate is in place to receive it; the natural follow-up file is Theories/Phonology/Process/AlternationSubregular.lean (or a small addition here once a Studies file consumes the classification).

def Phonology.Alternation.TierRule.predictFromCtx {α : Type} (r : TierRule α) : Option α → Option Bool

The prediction function shared by applyAt (under identity tier + left side) and the SFST construction: given an "accumulated last context" option, compute the feature value the rule predicts.

Equations

• One or more equations did not get rendered due to their size.
• r.predictFromCtx none = r.default

def Phonology.Alternation.TierRule.lastContextOf {α : Type} (r : TierRule α) (xs : List α) : Option α

The last context-matching segment of a list as Option α. State representation for the SFST below: the last input segment so far that satisfies targetIsContext.

Equations

• r.lastContextOf xs = (List.filter (fun (x : α) => decide (r.targetIsContext x)) xs).getLast?

def Phonology.Alternation.TierRule.toIdTierSFST {α : Type} (r : TierRule α) : Core.Computability.Subregular.Function.SFST (Option α) α (Option Bool)

SFST witness for the identity-tier, left-side applyToString: state tracks the last targetIsContext-matching input segment.

Equations

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

@[simp]

theorem Phonology.Alternation.TierRule.toIdTierSFST_step_fst {α : Type} (r : TierRule α) (st : Option α) (s : α) : (r.toIdTierSFST.step st s).fst = if r.targetIsContext s then some s else st

The SFST's state after one step matches the running lastContextOf.

@[simp]

theorem Phonology.Alternation.TierRule.toIdTierSFST_step_snd {α : Type} (r : TierRule α) (st : Option α) (s : α) : (r.toIdTierSFST.step st s).snd = [r.predictFromCtx st]

theorem Phonology.Alternation.TierRule.lastContextOf_append_singleton {α : Type} (r : TierRule α) (past : List α) (x : α) : r.lastContextOf (past ++ [x]) = if r.targetIsContext x then some x else r.lastContextOf past

lastContextOf extends by one step: appending a single segment to the past updates the running last-context exactly as the SFST step does.

theorem Phonology.Alternation.TierRule.applyAt_eq_predictFromCtx {α : Type} (r : TierRule α) (h_id : r.tier = Core.Tier.id) (h_side : r.side = Core.Direction.left) (past : List α) : r.applyAt past = r.predictFromCtx (r.lastContextOf past)

Under identity tier + left side, applyAt agrees with predictFromCtx ∘ lastContextOf — the structural rephrasing of id_tier_left_is_strict_local.

theorem Phonology.Alternation.TierRule.toIdTierSFST_runFrom_eq_applyToStringAux {α : Type} (r : TierRule α) (h_id : r.tier = Core.Tier.id) (h_side : r.side = Core.Direction.left) (past input : List α) : r.toIdTierSFST.runFrom (r.lastContextOf past) input = applyToString.applyToStringAux r input past

The SFST computes applyToString. Generalised over the SFST's starting state (which represents the lastContextOf of some virtual past) and the corresponding past.

theorem Phonology.Alternation.TierRule.applyToString_isLeftSubsequential_of_id_tier {α : Type} (r : TierRule α) (h_id : r.tier = Core.Tier.id) (h_side : r.side = Core.Direction.left) : Core.Computability.Subregular.Function.IsLeftSubsequential r.applyToString

Identity-tier left-side TierRules reify to Left-Subsequential functions. Closes audit D6 with a real witness construction (not a sorry): the SFST has state Option α (last-context-matching segment seen) and emits the rule's prediction at each step.