TierProjection-based rules (TierRule)

[Bel26] [Gol76]

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) Rel(A, F) / __ C ∘ proj(·, T) (right-context)

where:

• T ⊆ α is a tier (an erasing string-homomorphism — see TierProjection);
• 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 [Bel26]);
• 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 [Bel26]), Rose-Walker harmony systems (which structurally contain a TierRule as their value-prediction core — see Subregular.Harmony.System in Subregular/Harmony.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 Subregular/LocalRewrite.lean

Phonology/Subregular/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 Subregular.Relation : Type

Belth's Agree/Disagree distinction ([Bel26]).

• agree : Relation
• disagree : Relation

@[implicit_reducible]

instance Subregular.instDecidableEqRelation : DecidableEq Relation

Equations

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

@[implicit_reducible]

instance Subregular.instReprRelation : Repr Relation

Equations

• Subregular.instReprRelation = { reprPrec := Subregular.instReprRelation.repr }

def Subregular.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Subregular.instReprRelation.repr Subregular.Relation.agree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.Relation.agree")).group prec✝

def Subregular.Relation.flip : Relation → Relation

The relation flipped: .agree ↔ .disagree.

Equations

• Subregular.Relation.agree.flip = Subregular.Relation.disagree
• Subregular.Relation.disagree.flip = Subregular.Relation.agree

@[simp]

theorem Subregular.Relation.flip_flip (r : Relation) : r.flip.flip = r

Flipping the relation twice returns the original.

@[reducible, inline]

abbrev Subregular.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 Subregular.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

• Subregular.Side = Subregular.Direction

structure Subregular.TierRule (α : Type) : Type

A tier-based alternation rule over alphabet α: project the word onto a tier, find the adjacent context segment on side, and fill the target's feature by relation to it, falling back to default.

• tier : TierProjection α α

  The erasing projection ([Gol76]) onto which the context-class check is performed.

• side : Side

  Whether the triggering context precedes (.left) or follows (.right) the unspecified target slot.

• targetIsContext : α → Prop

  The natural class C: the rule fires only when the tier-adjacent segment satisfies this predicate.

• decTarget : DecidablePred self.targetIsContext

  Decidability of the context class, carried as an instance field (mathlib's Finset.filter convention).

• relation : Relation

  .agree (assimilation) or .disagree (dissimilation).

• featureValue : α → Option Bool

  The value of the alternating feature extracted from a context segment; none means the segment is itself underspecified, deferring to default.

• default : Option Bool

  The Elsewhere value ([Bel26]'s default fallback): some v is the concrete fallback when no context is found, none makes applyAt return none.

def Subregular.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 Subregular.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 Subregular.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 Subregular.TierRule.flipRelation_flipRelation {α : Type} (r : TierRule α) : r.flipRelation.flipRelation = r

Flipping the relation twice returns the original rule.

theorem Subregular.TierRule.id_tier_left_is_strict_local {α : Type} (r : TierRule α) (h_id : r.tier = TierProjection.id) (h_side : r.side = 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 (e.g. Turkish voicing assimilation, Agree([?voice], {voice}) / [*] __ over the trivial projection — [Bel26]).

def Subregular.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 = Subregular.TierRule.applyToString.applyToStringAux r input []

def Subregular.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

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

Function-level subregular classification

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 [ARGH20]:

• 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 → TierProjection-Subsequential (a strictly larger class than Left-Subsequential, captured by the standard Heinz-Rawski-Tanner 2011 tier-strictly-local family applied to function classes).

The non-trivial-tier classification is deferred (the SFST witness needs to thread the tier projection's state alongside the predicate-evaluation state); the identity-tier case is discharged below. Land the general witness here once a Studies file consumes it.

def Subregular.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 Subregular.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 Subregular.TierRule.toIdTierSFST {α : Type} (r : TierRule α) : SFST α (Option Bool) (Option α)

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 Subregular.TierRule.toIdTierSFST_step_fst {α : Type} (r : TierRule α) (st : Option α) (s : α) : (r.toIdTierSFST.step st s).1 = if r.targetIsContext s then some s else st

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

@[simp]

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

theorem Subregular.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 Subregular.TierRule.applyAt_eq_predictFromCtx {α : Type} (r : TierRule α) (h_id : r.tier = TierProjection.id) (h_side : r.side = 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 Subregular.TierRule.toIdTierSFST_runFrom_eq_applyToStringAux {α : Type} (r : TierRule α) (h_id : r.tier = TierProjection.id) (h_side : r.side = 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 Subregular.TierRule.applyToString_isLeftSubsequential_of_id_tier {α : Type} [Fintype α] (r : TierRule α) (h_id : r.tier = TierProjection.id) (h_side : r.side = Direction.left) : 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.

Myopia: the tier-rule prediction has no look-ahead

theorem Subregular.TierRule.applyToStringAux_getElem? {α : Type} (r : TierRule α) (input past : List α) (i : ℕ) : (applyToString.applyToStringAux r input past)[i]? = if i < input.length then some (r.applyAt (past ++ List.take i input)) else none

applyToString's coordinate i is the rule's prediction over the strict input prefix: applyAt r (input.take i) (in range; none otherwise).

theorem Subregular.TierRule.applyToString_getElem? {α : Type} (r : TierRule α) (u : List α) (i : ℕ) : (r.applyToString u)[i]? = if i < u.length then some (r.applyAt (List.take i u)) else none

theorem Subregular.TierRule.applyToString_prefixDetermined {α : Type} (r : TierRule α) (i : ℕ) : OutputDependsOn r.applyToString i {k : ℕ | k < i}

applyToString is prefix-determined: its i-th output is fixed by the input's strict prefix {k | k < i}.

theorem Subregular.TierRule.applyToString_isRightMyopic {α : Type} (r : TierRule α) : IsMyopicTowards r.applyToString Direction.right

The tier-rule prediction mechanism is right-myopic — it has no look-ahead. Consequently no tier-rule-based prediction (the formal core of a Harmony.System) can compute a non-myopic harmony, such as an unbounded-circumambient pattern.