Belth (2026): A Learning-Based Account of Phonological Tiers @cite{belth-2026} #

D2L (Distant-to-Local) is an iterative learner that constructs phonological tiers as a byproduct of trying to express alternations as adjacent dependencies. Given underlying-form / surface-form pairs, D2L starts by projecting all segments and tries to predict the alternating segment from its linear neighbours. When the resulting rule fails Yang's Tolerance Principle @cite{yang-2016}, D2L deletes the offending segments from the tier and tries again, until either a tolerated rule is found or no further deletion helps.

The output of D2L is a tier-based alternation rule, modelled here by the canonical Phonology.Alternation.TierRule schema (in Theories/Phonology/Alternation.lean); the closely-related SPE non-tier Phonology.LocalRewrite.Rule schema in Theories/Phonology/Process/LocalRewrite.lean is the right substrate when the alternation does not factor through a tier projection. The function-level subregular classification of D2L outputs lives in Core/Computability/Subregular/Function/: tier-mediated dissimilation rules of the form Belth converges to are Tier-Subsequential (@cite{aksenova-rawski-graf-heinz-2020}). For Latin -alis / -aris allomorphy (@cite{belth-2026} §5.3, rule 54), the rule D2L converges to is

Disagree([?lat], {lat}) / [+cons] __ ∘ proj(·, [+cons]),

i.e. dissimilation of the underspecified affix-initial liquid /L/ from the immediately preceding [+cons] tier segment. @cite{belth-2026} reports 0.97 accuracy on a 121-word Perseus dataset; the residual ~3% errors are tolerated by Yang's Tolerance Principle (4 ≤ 121/ln 121), so D2L converges to this rule rather than memorizing the lexicon.

This study formalizes:

the rule (latinDissimRule) and its predictions on six worked examples (Belth ex. 5/53): navalis, popularis, pluvalis, floralis, legalis, lunaris;
the genuine empirical limit: lunaris surfaces with [r], but the [+cons]-tier rule predicts [l] (the immediately preceding tier segment is the nasal /n/, which is [−lat], so Disagree outputs [+lat]). This is one of the ~3% errors the Tolerance Principle tolerates;
a Tolerance-Principle certificate (latinDissimRule_tolerated_on_examples) showing the 1-of-6 exception count on this corpus is well under Yang's threshold;
a Subregular bridge (consTier_apply_eq_tierProject) grounding the consonant tier in the @cite{lambert-2022}/@cite{heinz-rawal-tanner-2011} TSL formalism;
an OCP-on-tier OT constraint (latinOCP, via Phonology.Constraints.mkOCPOnTier) and an OT tableau bridge: each empirical contrast becomes a winner-loser pair, tableauERC extracts the Elementary Ranking Condition (@cite{merchant-riggle-2016}), and the OT analysis is shown to track the rule-based analysis exactly, including the same lunaris failure (the lunaris ERC is contradictory on the two-constraint inventory ⟨OCP, *r⟩, which is the OT-side analogue of the rule's underextension).

D2L's Turkish (Belth §5.1) and Finnish (§5.2) rules are sketched in §10 below. They require multi-feature dependencies and explicit Elsewhere defaults; both extensions are admittable on demand.

On verification scope. D2L itself — the learning algorithm — is not run inside Lean. Belth's empirical claim is that, given a corpus, D2L converges to specific rules. Verifying that claim end-to-end would require running D2L on naturalistic datasets (CHILDES, MorphoChallenge, Perseus), which is out of scope for a Lean formalization. We instead formalize the learned rules and verify their predictions on representative examples, plus the Tolerance Principle inequality that licenses convergence.