[Lam26]: Multitier phonotactics with logic and algebra

Lambert (2026) classifies attested phonotactic constraints — bounded and unbounded stress, harmony, and tone across ~13 languages — into the multitier (Boolean closure of tier-projected) extensions of definite, generalized definite, and finite-or-cofinite classes. Headline empirical claims:

• Uyghur backness harmony is multitier definite (BTD) — strictly weaker than the multiple-tier-based strictly local class of [DSG19], settling (categorically) the challenge raised by [MM18].
• Karanga Shona tone is multitier generalized definite (BTLI) — no more complex than the default-to-opposite unbounded stress patterns, refining the melody-local analysis of [Jar20].

The propositional logic is IsBTC 𝒞 — the Boolean closure of IsTierBased 𝒞 — for 𝒞 in {IsDefinite k, IsGeneralizedDefinite k, Language.IsStrictlyLocal · k, Language.IsStrictlyPiecewise · k, IsFiniteOrCofinite}; the algebraic side is the syntactic-semigroup characterization of each class via Eilenberg [Eil76] variety equations (e.g., D = ⟦sx̄ = x̄⟧, ℒℐ = ⟦x^ω y x^ω z x^ω = x^ω y x^ω⟧ per [Str85] and [Alm95]). The Lean substrate (IsBTC, IsTierBased) lives in Subregular/Language/Multitier.lean; the algebraic characterization is queued for a future SyntacticMonoid PR.

Disclaimer 1: McCollum (2019) Uyghur gradience (linglib audit)

This disclaimer is not a scope qualification carried by Lambert (2026); the paper does not cite McCollum. It is a linglib-internal audit annotation: Lambert's BTD analysis is faithful to [MM18]'s categorical idealization, and a separate literature line — [McC19a] — argues the suffix backness assignment is not categorical in the way the multitier-definite formula requires. The "arbitrarily specified, statistical tendency to be back" clause that Mayer & Major report for the no-V no-C case is precisely the locus where McCollum's gradient data resists categorical analysis. The headline theorem uyghur_backness_isBTD characterizes the categorical pattern only; the gradience is out of scope.

Disclaimer 2: Karanga Shona scope restriction

The BTLI analysis applies to the verb-stem domain (post-hyphen material in Lambert (2026) (45)). [Jar20]'s motivation for a melody local class extends across morphological boundaries and to longer melodic patterns; the BTLI characterization is not a refutation of the broader melody-local programme but a delimited result for the verb-stem surface pattern. The headline theorem karanga_shona_verb_stem_isBTLI is named accordingly.

Cross-framework dialogue

The multitier substrate is the prohibition reading of constraints scaled to Boolean closure. Cross-references the new file makes explicit (rather than silently diverging from existing linglib formalizations):

• OT: linglib's Constraint framework places no complexity bound; Lambert says all phonotactics live in IsBTC. The supraregular counter-witness theorem and the positive mkForbidPairsOnTier ⊆ TSL_2 theorem are queued for a future Phonology/Subregular/OTBound.lean.
• Harmonic Serialism: Studies/McPhersonLamont2026.lean proves Poko surface tone HS-derivable but parallel-OT-impossible. Lambert's static BTC characterization, applied to Poko's surface stringset, would clarify static description ≠ alternation explanation. Cross-reference to be added when Poko's surface stringset is independently classified.
• Autosegmental: linglib's Phonology/Autosegmental/{ RegisterTier, GrammaticalTone}.lean formalize multiply-linked tone representations. Lambert (2026) §5 self-confesses that string-based analysis loses information for tone; the loss theorem is stated as lambert_string_input_loses_tone_associations (sorry'd) below.
• OCP: Phonology/Subregular/OCP.lean carries a prohibition-vs-merger distinction; IsBTC is the mathematical home of the prohibition family at scale. The OCP file's docstring should gain a "see also: BTC" link in a follow-up retrofit.
• Structure-sensitive MTSL [DSG19]: not formalized in linglib. Lambert's "BTD strictly supersedes SS-MTSL on Uyghur" is recorded as a TODO theorem (btd_supersedes_ss_mtsl_on_uyghur) for when SS-MTSL substrate lands.

Audit calibration note

Per linglib's domain-expert agent calibration: the McCollum-2019 and Karanga-Shona-scope concerns are flagged HIGH but should be treated PROVISIONAL — they are corrections to scope, not refutations of the formal results. The Lean theorems below state the formal claims; the empirical disclaimers live in this docstring and the per-theorem docstrings.

Sandwich-word helpers

The Tsuut'ina/Luganda counterexamples below are bookended words replicate kL aL ++ mid ++ replicate kR aR. These thin local wrappers specialise the generic List bookend lemmas (Core/Data/List/Bookend.lean) to the Edge-projection view used in the proofs.

inductive Lambert2026.IbanSyl : Type

Iban syllable type [Oma69]: stressed (σ́) or unstressed (σ). The two-letter alphabet of Lambert (2026) §2.1.

• unstressed : IbanSyl
• stressed : IbanSyl

@[implicit_reducible]

instance Lambert2026.instDecidableEqIbanSyl : DecidableEq IbanSyl

Equations

• Lambert2026.instDecidableEqIbanSyl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Lambert2026.instReprIbanSyl : Repr IbanSyl

Equations

• Lambert2026.instReprIbanSyl = { reprPrec := Lambert2026.instReprIbanSyl.repr }

def Lambert2026.instReprIbanSyl.repr : IbanSyl → ℕ → Std.Format

Equations

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

def Lambert2026.ibanLang : Language IbanSyl

The Iban stress-final language [Oma69]: the right-edge D_1 language whose permitted length-1 suffix is [stressed].

Equations

• Lambert2026.ibanLang = {w : List Lambert2026.IbanSyl | Subregular.Edge.right.takeAt 1 w ∈ {[Lambert2026.IbanSyl.stressed]}}

theorem Lambert2026.iban_isDefinite_one : ibanLang.IsDefinite 1

Iban stress-final ∈ D_1 (Lambert 2026 §2.1, paper p. 4 example (2)).

def Lambert2026.amaraLang : Language IbanSyl

Amara stress [Thu66]: penultimate-syllable stress with the monosyllabic exception (single syllable bears stress). The D_2 language whose permitted length-2 suffixes are a stressed monosyllable or a stressed-then- unstressed penult.

Equations

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

theorem Lambert2026.amara_isDefinite_two : amaraLang.IsDefinite 2

Amara stress-penult ∈ D_2 (Lambert 2026 §2.1).

def Lambert2026.finnishLang : Language IbanSyl

The Finnish stress-initial language [STY08]: primary stress fixed to the initial syllable — the reverse-definite dual of Iban, the left-edge RD_1 language whose permitted length-1 prefix is [stressed] [Lam26] §2.2.

Equations

• Lambert2026.finnishLang = {w : List Lambert2026.IbanSyl | Subregular.Edge.left.takeAt 1 w ∈ {[Lambert2026.IbanSyl.stressed]}}

theorem Lambert2026.finnish_isReverseDefinite_one : finnishLang.IsReverseDefinite 1

Finnish stress-initial ∈ K_1 (Lambert 2026 §2.2, paper p. 5 example (6)).

inductive Lambert2026.UyghurSeg : Type

Uyghur segment classes relevant to backness harmony [MM18] [Lam26] (33)-(35): front vowels, back vowels, transparent (i, e), front dorsal consonants, back dorsal consonants, suffix-marked harmonizing vowels and consonants, and a residual "other" class for non-harmonizing material.

• frontVowel : UyghurSeg
• backVowel : UyghurSeg
• transparentVowel : UyghurSeg
• frontDorsal : UyghurSeg
• backDorsal : UyghurSeg
• suffixFrontVowel : UyghurSeg
• suffixBackVowel : UyghurSeg
• suffixFrontDorsal : UyghurSeg
• suffixBackDorsal : UyghurSeg
• other : UyghurSeg

@[implicit_reducible]

instance Lambert2026.instDecidableEqUyghurSeg : DecidableEq UyghurSeg

Equations

• Lambert2026.instDecidableEqUyghurSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lambert2026.instReprUyghurSeg.repr : UyghurSeg → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Lambert2026.instReprUyghurSeg : Repr UyghurSeg

Equations

• Lambert2026.instReprUyghurSeg = { reprPrec := Lambert2026.instReprUyghurSeg.repr }

Tier predicates

Lambert's V_f ∪ V_b is the harmonising-vowel tier; C_f ∪ C_b is the dorsal tier; S_f and S_b are the front- and back-suffix tiers (V_X ∪ C_X marked as suffix). Each is a Boolean predicate on UyghurSeg.

def Lambert2026.isHarmonyingVowel : UyghurSeg → Bool

Harmonising-vowel tier: V_f ∪ V_b.

Equations

• Lambert2026.isHarmonyingVowel Lambert2026.UyghurSeg.frontVowel = true
• Lambert2026.isHarmonyingVowel Lambert2026.UyghurSeg.backVowel = true
• Lambert2026.isHarmonyingVowel x✝ = false

def Lambert2026.isDorsal : UyghurSeg → Bool

Dorsal-consonant tier: C_f ∪ C_b.

Equations

• Lambert2026.isDorsal Lambert2026.UyghurSeg.frontDorsal = true
• Lambert2026.isDorsal Lambert2026.UyghurSeg.backDorsal = true
• Lambert2026.isDorsal x✝ = false

def Lambert2026.isSuffixFront : UyghurSeg → Bool

Front-suffix tier S_f: front-marked suffix material (vowel or dorsal).

Equations

• Lambert2026.isSuffixFront Lambert2026.UyghurSeg.suffixFrontVowel = true
• Lambert2026.isSuffixFront Lambert2026.UyghurSeg.suffixFrontDorsal = true
• Lambert2026.isSuffixFront x✝ = false

def Lambert2026.isSuffixBack : UyghurSeg → Bool

Back-suffix tier S_b: back-marked suffix material (vowel or dorsal).

Equations

• Lambert2026.isSuffixBack Lambert2026.UyghurSeg.suffixBackVowel = true
• Lambert2026.isSuffixBack Lambert2026.UyghurSeg.suffixBackDorsal = true
• Lambert2026.isSuffixBack x✝ = false

Atomic tier-projected definite languages

Each of the four atomic predicates in (35) is a IsTierBased (Language.IsDefinite · 1) test: a single permitted length-1 suffix set on the filtered tier (Language.isDefinite_setOf_right), lifted via IsTierBased.

def Lambert2026.tierEmptyLang (T : UyghurSeg → Bool) : Language UyghurSeg

The language "tier T is empty": after filtering by T, the word is []. Encoded as IsTierBased (IsDefinite 1) via the singleton 1-suffix {[]} (the only word whose right-1-suffix is [] is the empty word).

Equations

• Lambert2026.tierEmptyLang T = {w : List Lambert2026.UyghurSeg | List.filter T w = []}

def Lambert2026.tierEndsWithLang (T : UyghurSeg → Bool) (x : UyghurSeg) : Language UyghurSeg

The language "tier T ends with x": after filtering by T, the word's last element is x. Encoded as IsTierBased (IsDefinite 1) via the singleton 1-suffix {[x]}.

Equations

• Lambert2026.tierEndsWithLang T x = {w : List Lambert2026.UyghurSeg | List.drop ((List.filter T w).length - 1) (List.filter T w) = [x]}

theorem Lambert2026.tierEmptyLang_isTierBased (T : UyghurSeg → Bool) : Language.IsTierBased (fun (x : Language UyghurSeg) => x.IsDefinite 1) (tierEmptyLang T)

tierEmptyLang T is in IsTierBased (IsDefinite 1). The base 1-definite language is the singleton {[]} (only [] has right-1- suffix []).

theorem Lambert2026.tierEndsWithLang_isTierBased (T : UyghurSeg → Bool) (x : UyghurSeg) : Language.IsTierBased (fun (x : Language UyghurSeg) => x.IsDefinite 1) (tierEndsWithLang T x)

tierEndsWithLang T x is in IsTierBased (IsDefinite 1). The base 1-definite language is the singleton {[x]}.

The Uyghur backness language as conjunction of (35a)-(35b)

The English implication A → B is Boolean Aᶜ ∨ B; written using mathlib's Language lattice (Boolean algebra), Aᶜ ⊔ B. The full language is the intersection of four such implications.

def Lambert2026.uyghurBacknessLang : Language UyghurSeg

The Uyghur backness harmony language as the conjunction of the four implications in Lambert (2026) (35a)-(35b). Categorical idealisation — see file docstring for the [McC19a] gradience disclaimer.

Equations

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

theorem Lambert2026.uyghur_backness_isBTD : ∃ (k : ℕ), Language.IsBTD k uyghurBacknessLang

Uyghur backness harmony ∈ BTD₁ (Lambert 2026 §4.3, eq. (35), refining [MM18]). Constructive witness: the formalised uyghurBacknessLang is the intersection of four implications, each Aᶜ ⊔ B where A and B are IsTierBased (IsDefinite 1) (each is a tier-projected single-suffix test). The BTD membership follows from IsBTC.{base, compl, union, inter} applied to the four atomic tier-projected definite languages.

inductive Lambert2026.KShoTone : Type

Karanga Shona tone alphabet [Odd84] [Lam26] §5.6: low (ℓ) and high (h).

• low : KShoTone
• high : KShoTone

@[implicit_reducible]

instance Lambert2026.instDecidableEqKShoTone : DecidableEq KShoTone

Equations

• Lambert2026.instDecidableEqKShoTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Lambert2026.instReprKShoTone : Repr KShoTone

Equations

• Lambert2026.instReprKShoTone = { reprPrec := Lambert2026.instReprKShoTone.repr }

def Lambert2026.instReprKShoTone.repr : KShoTone → ℕ → Std.Format

Equations

• Lambert2026.instReprKShoTone.repr Lambert2026.KShoTone.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lambert2026.KShoTone.low")).group prec✝
• Lambert2026.instReprKShoTone.repr Lambert2026.KShoTone.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lambert2026.KShoTone.high")).group prec✝

Atomic IsGeneralizedDefinite languages (uniform k = 5)

Each component of Lambert's φ_F ∨ L_m ∨ H_m reduces to a Boolean combination of edge-anchored substring tests and tier-projected substring tests. We encode each as a Language KShoTone and prove it's IsGeneralizedDefinite 5 directly via List.take_take / List.drop_drop-style structural arguments. The uniform k = 5 is chosen as 1 + max(prefix length, suffix length, tier-projection length, max φ_F word length) = 1 + 4.

def Lambert2026.startsWithLang {α : Type u_1} (xs : List α) : Language α

"Word starts with xs": the language {w | w.take xs.length = xs}. Originally introduced for KShoTone but α-generic; also reused for LugandaTone in §10 Kagoshima Japanese.

Equations

• Lambert2026.startsWithLang xs = {w : List α | List.take xs.length w = xs}

def Lambert2026.endsWithLang {α : Type u_1} (xs : List α) : Language α

"Word ends with xs": the language {w | w.drop (w.length - xs.length) = xs}. α-generic, reused for LugandaTone in §10 Kagoshima Japanese.

Equations

• Lambert2026.endsWithLang xs = {w : List α | List.drop (w.length - xs.length) w = xs}

def Lambert2026.tierEqualLang {α : Type u_1} (T : α → Bool) (xs : List α) : Language α

"Tier-projection by T equals exactly xs": the language {w | w.filter T = xs}. α-generic, reused for LugandaTone in §10 Kagoshima Japanese.

Equations

• Lambert2026.tierEqualLang T xs = {w : List α | List.filter T w = xs}

def Lambert2026.isHigh : KShoTone → Bool

Boolean tier predicate for h-tier (high tones only).

Equations

• Lambert2026.isHigh Lambert2026.KShoTone.high = true
• Lambert2026.isHigh Lambert2026.KShoTone.low = false

IsGeneralizedDefinite witnesses at k = 5

Unfolding helper: Edge.left.takeAt k w = w.take k and Edge.right.takeAt k w = w.drop (w.length - k) by rfl. The hypotheses from IsGeneralizedDefinite k come in the Edge.takeAt form; we unfold via show at the top of each proof.

theorem Lambert2026.startsWithLang_isGenDef {α : Type u_1} (xs : List α) (k : ℕ) (hk : xs.length ≤ k) : (startsWithLang xs).IsGeneralizedDefinite k

startsWithLang xs is IsGeneralizedDefinite k for any k ≥ xs.length. Proof: same k-prefix on both words determines the xs.length-prefix via List.take_take. α-generic.

theorem Lambert2026.endsWithLang_isGenDef {α : Type u_1} (xs : List α) (k : ℕ) (hk : xs.length ≤ k) : (endsWithLang xs).IsGeneralizedDefinite k

endsWithLang xs is IsGeneralizedDefinite k for any k ≥ xs.length. Symmetric to startsWithLang_isGenDef; the underlying identity is w.drop (w.length - xs.length) = (w.drop (w.length - k)).drop (k - xs.length) when xs.length ≤ k ≤ w.length. The general case splits on whether w is shorter than k.

theorem Lambert2026.tierEqualLang_isTierBased {α : Type u_1} (T : α → Bool) (xs : List α) (k : ℕ) (hk : xs.length < k) : Language.IsTierBased (fun (x : Language α) => x.IsGeneralizedDefinite k) (tierEqualLang T xs)

tierEqualLang T xs is IsTierBased (IsGeneralizedDefinite k) for any k > xs.length (strict — without strictness, e.g. {[h, h]} is not GeneralizedDefinite 2 since [h, h, h] and [h, h] share both 2-prefix and 2-suffix).

def Lambert2026.kshonaSevenWords : List (List KShoTone)

The seven fully specified words from Lambert (2026) §5.6 (just above eq. (46), paper p. 19). Max length 4 (hhℓh).

Equations

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

def Lambert2026.phi_F : Language KShoTone

The finite-language part φ_F of Lambert's witness — the seven fully specified words.

Equations

• Lambert2026.phi_F = {w : List Lambert2026.KShoTone | w ∈ Lambert2026.kshonaSevenWords}

theorem Lambert2026.phi_F_isGenDef : phi_F.IsGeneralizedDefinite 5

phi_F is IsGeneralizedDefinite 5. Max word length is 4, so for k = 5 > 4, any word of length ≤ 4 has k-prefix = whole word. Two words with same 5-prefix and length ≤ 4 are equal; any word with length > 4 has a 5-prefix of length 5 (or whole) which differs from any short word's 5-prefix.

def Lambert2026.karangaShonaVerbStemLang : Language KShoTone

The Karanga Shona verb-stem tone language as the disjunction φ_F ∨ L_m ∨ H_m from Lambert (2026) §5.6 (formula appearing just after eq. (49), paper p. 19).

Equations

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

theorem Lambert2026.karanga_shona_verb_stem_isBTLI : ∃ (k : ℕ), Language.IsBTLI k karangaShonaVerbStemLang

Karanga Shona verb-stem tone ∈ BTLI₅ (Lambert 2026 §5.6, refining [Jar20]). Constructive witness for the disjunction φ_F ∨ L_m ∨ H_m at uniform k = 5. Each disjunct lifts to IsBTC (IsGeneralizedDefinite 5) via IsTierBased.of_class + IsBTC.base; the disjunction is closed by IsBTC.union.

Sibilant-harmony grammars over the shared Sibilant alphabet

Both asymmetric directions plus the symmetric foil, over the shared Subregular.Sibilant substrate. Lambert's classification draws the symmetric-vs-asymmetric comparison: the symmetric grammar is the [Han10] Navajo profile (TSLGrammar.agree, disagreement forbidden in both directions), the anterior-first asymmetric grammar the [Coo78] Tsuut'ina profile.

def Lambert2026.antPostForbidden : Subregular.Sibilant → Subregular.Sibilant → Prop

Forbidden-pair relation: anterior immediately preceding posterior on the tier (the [Coo78] Tsuut'ina adjacency).

Equations

• Lambert2026.antPostForbidden Subregular.Sibilant.anterior Subregular.Sibilant.posterior = True
• Lambert2026.antPostForbidden x✝¹ x✝ = False

@[implicit_reducible]

instance Lambert2026.instDecidableRelSibilantAntPostForbidden : DecidableRel antPostForbidden

Equations

• Lambert2026.instDecidableRelSibilantAntPostForbidden Subregular.Sibilant.anterior Subregular.Sibilant.posterior = isTrue trivial
• Lambert2026.instDecidableRelSibilantAntPostForbidden Subregular.Sibilant.anterior Subregular.Sibilant.anterior = isFalse not_false
• Lambert2026.instDecidableRelSibilantAntPostForbidden Subregular.Sibilant.anterior Subregular.Sibilant.neutral = isFalse not_false
• Lambert2026.instDecidableRelSibilantAntPostForbidden Subregular.Sibilant.posterior x✝ = isFalse not_false
• Lambert2026.instDecidableRelSibilantAntPostForbidden Subregular.Sibilant.neutral x✝ = isFalse not_false

def Lambert2026.asymmetricHarmonyAntFirst : Subregular.TSLGrammar 2 Subregular.Sibilant

Tsuut'ina-style asymmetric harmony: anterior-before-posterior forbidden on the tier, the reverse permitted.

Equations

• Lambert2026.asymmetricHarmonyAntFirst = Subregular.TSLGrammar.ofForbiddenPairs Lambert2026.antPostForbidden Subregular.Sibilant.onTier

def Lambert2026.postAntForbidden : Subregular.Sibilant → Subregular.Sibilant → Prop

Dual forbidden-pair relation: posterior immediately preceding anterior.

Equations

• Lambert2026.postAntForbidden Subregular.Sibilant.posterior Subregular.Sibilant.anterior = True
• Lambert2026.postAntForbidden x✝¹ x✝ = False

@[implicit_reducible]

instance Lambert2026.instDecidableRelSibilantPostAntForbidden : DecidableRel postAntForbidden

Equations

• Lambert2026.instDecidableRelSibilantPostAntForbidden Subregular.Sibilant.posterior Subregular.Sibilant.anterior = isTrue trivial
• Lambert2026.instDecidableRelSibilantPostAntForbidden Subregular.Sibilant.posterior Subregular.Sibilant.posterior = isFalse not_false
• Lambert2026.instDecidableRelSibilantPostAntForbidden Subregular.Sibilant.posterior Subregular.Sibilant.neutral = isFalse not_false
• Lambert2026.instDecidableRelSibilantPostAntForbidden Subregular.Sibilant.anterior x✝ = isFalse not_false
• Lambert2026.instDecidableRelSibilantPostAntForbidden Subregular.Sibilant.neutral x✝ = isFalse not_false

def Lambert2026.asymmetricHarmonyPostFirst : Subregular.TSLGrammar 2 Subregular.Sibilant

Posterior-first asymmetric harmony grammar (the mirror of asymmetricHarmonyAntFirst).

Equations

• Lambert2026.asymmetricHarmonyPostFirst = Subregular.TSLGrammar.ofForbiddenPairs Lambert2026.postAntForbidden Subregular.Sibilant.onTier

def Lambert2026.symmetricHarmony : Subregular.TSLGrammar 2 Subregular.Sibilant

Symmetric sibilant harmony: any tier-adjacent disagreement forbidden — the [Han10] Navajo profile, the foil for the asymmetric comparison.

Equations

• Lambert2026.symmetricHarmony = Subregular.TSLGrammar.agree Subregular.Sibilant.onTier

theorem Lambert2026.symmetricHarmony_lang_subset_asymAntFirst : symmetricHarmony.lang ≤ asymmetricHarmonyAntFirst.lang

The symmetric language is contained in the anterior-first asymmetric language: forbidding disagreement in both directions rules out everything the one-direction constraint does, and more.

theorem Lambert2026.symmetricHarmony_lang_subset_asymPostFirst : symmetricHarmony.lang ≤ asymmetricHarmonyPostFirst.lang

Dual inclusion against the posterior-first asymmetric language.

@[reducible, inline]

abbrev Lambert2026.TsuutinaSeg : Type

The Tsuut'ina sibilant alphabet ([Coo78]) is the shared three-class Subregular.Sibilant (anterior s, posterior ʃ, neutral non-sibilant).

Equations

• Lambert2026.TsuutinaSeg = Subregular.Sibilant

def Lambert2026.tsuutinaTSLGrammar : Subregular.TSLGrammar 2 TsuutinaSeg

The TSL_2 grammar for Tsuut'ina asymmetric sibilant harmony ([Coo78]; Lambert's asymmetric classification): anterior preceding posterior on the sibilant tier is forbidden, the reverse permitted.

Equations

• Lambert2026.tsuutinaTSLGrammar = Lambert2026.asymmetricHarmonyAntFirst

def Lambert2026.tsuutinaLang : Language TsuutinaSeg

The Tsuut'ina asymmetric sibilant harmony language. Defined as the language of the TSL_2 witness so that the membership theorem is definitional.

Equations

• Lambert2026.tsuutinaLang = Lambert2026.tsuutinaTSLGrammar.lang

theorem Lambert2026.tsuutina_isTSL2 : Language.IsTierStrictlyLocal 2 tsuutinaLang

Tsuut'ina asymmetric harmony ∈ TSL_2. Definitional witness: the TSL_2 grammar tsuutinaTSLGrammar.

Refutation: Tsuut'ina ∉ BTLI

Lambert's parameterised counterexample: for every k, the words ʃᵏ⁺¹sᵏ⁺¹ (accepted) and ʃᵏ s ʃ sᵏ (rejected) share the length-k tier-prefix and length-k tier-suffix on every Bool tier. Both witnesses are sandwiches with asymmetric bookends posterior on the left and anterior on the right; widths differ between witnesses (k+1 for accepted, k for rejected). The 8-tier enumeration (3 alphabet classes × 2 keep/drop) collapses to 4 since the witnesses contain no neutrals.

The local sandwich helpers (over Core/Data/List/Bookend.lean) handle the (true, true) case directly via takeAt_*_sandwich (the bookends are wide enough); the other three cases reduce to filtered words being equal (after a replicate_succ rewrite to merge the middle contribution into the bookend).

@[reducible, inline]

abbrev Lambert2026.tsuutinaAccepted (k : ℕ) : List TsuutinaSeg

The accepted Tsuut'ina parameterised witness ʃᵏ⁺¹ sᵏ⁺¹. Sibilant tier projection: posterior^(k+1) ++ anterior^(k+1) — no anterior precedes any posterior.

Equations

• Lambert2026.tsuutinaAccepted k = Lambert2026.sandwich✝ (k + 1) Subregular.Sibilant.posterior [] (k + 1) Subregular.Sibilant.anterior

@[reducible, inline]

abbrev Lambert2026.tsuutinaRejected (k : ℕ) : List TsuutinaSeg

The rejected Tsuut'ina parameterised witness ʃᵏ s ʃ sᵏ. The internal [anterior, posterior] is the forbidden adjacency on the sibilant tier.

Equations

• Lambert2026.tsuutinaRejected k = Lambert2026.sandwich✝ k Subregular.Sibilant.posterior [Subregular.Sibilant.anterior, Subregular.Sibilant.posterior] k Subregular.Sibilant.anterior

theorem Lambert2026.tsuutina_not_isBTLI (k : ℕ) : ¬Language.IsBTLI k tsuutinaLang

Tsuut'ina asymmetric harmony ∉ BTLI (Lambert's parametrised counterexample).

inductive Lambert2026.LugandaTone : Type

Luganda tone alphabet [HK10]: low (ℓ) and high (h), following [Jar20]'s identification of "intermediate" with low in the input.

• low : LugandaTone
• high : LugandaTone

@[implicit_reducible]

instance Lambert2026.instDecidableEqLugandaTone : DecidableEq LugandaTone

Equations

• Lambert2026.instDecidableEqLugandaTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lambert2026.instReprLugandaTone.repr : LugandaTone → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Lambert2026.instReprLugandaTone : Repr LugandaTone

Equations

• Lambert2026.instReprLugandaTone = { reprPrec := Lambert2026.instReprLugandaTone.repr }

def Lambert2026.lugandaPred (w : List LugandaTone) : Prop

The Luganda high-tone plateauing predicate [Lam26] (37): no [h, ℓ, h] subsequence (at most one high span), and if any high tone appears then there is a later low ([h, ℓ] is a subsequence).

Equations

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

def Lambert2026.lugandaLang : Language LugandaTone

The Luganda high-tone plateauing language.

Equations

• Lambert2026.lugandaLang = {w : List Lambert2026.LugandaTone | Lambert2026.lugandaPred w}

@[simp]

theorem Lambert2026.mem_lugandaLang (w : List LugandaTone) : w ∈ lugandaLang ↔ lugandaPred w

Membership in lugandaLang is membership in lugandaPred.

theorem Lambert2026.luganda_isPT : lugandaLang.IsPiecewiseTestable 3

Luganda high-tone plateauing ∈ PT_3 (Lambert 2026 (37)). The predicate depends only on length-≤-3 subsequence presence: the length-3 [h, ℓ, h], the length-2 [h, ℓ], and the length-1 [h].

The proof reduces each conjunct of lugandaPred to the corresponding subseqSet 3 membership question, then transfers via subseqSet_eq_iff.

Refutation: Luganda ∉ BTLI

Lambert (2026) §5.1 parameterised counterexample: for every k, the words ℓᵏ ℓ h h ℓ ℓᵏ (accepted) and ℓᵏ ℓ h ℓ h ℓ ℓᵏ (rejected) share the length-k tier-prefix and length-k tier-suffix on every Bool tier. Both witnesses are sandwiches with bookend low and width k; the local sandwich helpers (over Core/Data/List/Bookend.lean) handle the bookend-keeps-tier-affix case directly, leaving only the small filtered-middle equality as per-witness work.

Membership separation is predicate-level (not TSL-grammar level): lugandaPred requires no [h, ℓ, h] subsequence and (if any high appears) a [h, ℓ] subsequence. Accepted satisfies both; rejected fails the first because its explicit middle [ℓ, h, ℓ, h, ℓ] contains [h, ℓ, h] as a subsequence.

@[reducible, inline]

abbrev Lambert2026.lugandaAccepted (k : ℕ) : List LugandaTone

The accepted Luganda parameterised witness ℓᵏ ℓ h h ℓ ℓᵏ. The two high tones are adjacent inside the middle, so no [h, ℓ, h] subsequence can be formed (no low position lies strictly between them).

Equations

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

@[reducible, inline]

abbrev Lambert2026.lugandaRejected (k : ℕ) : List LugandaTone

The rejected Luganda parameterised witness ℓᵏ ℓ h ℓ h ℓ ℓᵏ. The explicit middle [ℓ, h, ℓ, h, ℓ] contains [h, ℓ, h] as a subsequence — exactly the structural pattern lugandaPred forbids.

Equations

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

theorem Lambert2026.luganda_not_isBTLI (k : ℕ) : ¬Language.IsBTLI k lugandaLang

Luganda high-tone plateauing ∉ BTLI (Lambert 2026 §5.1). Parametrised-word witness: ℓᵏ ℓ h h ℓ ℓᵏ is accepted while ℓᵏ ℓ h ℓ h ℓ ℓᵏ is rejected, but the two share all length-k tier-affixes on every tier.

Lambert 2026 §5.2 ([Din06]): Prinmi pitch-accent lexically selects a high-tone position within a domain (morpheme or span of adjacent morphemes); high may spread progressively to the next syllable. The resulting pattern enforces:

1. Obligatoriness: at least one high tone (h).
2. At most one high span: no [h, ℓ, h] subsequence (same as Luganda §5.1).
3. Span length ≤ 2: no [h, h, h] subsequence (new conjunct not present in Luganda).

Lambert: "the same words witness this nonmembership as for high-tone plateauing: ℓᵏ h h ℓᵏ is valid but ℓᵏ h ℓ h ℓᵏ is not, despite the two having the same k-affixes on every tier." So we reuse lugandaAccepted / lugandaRejected as witnesses and luganda_tierAffixes as the indistinguishability proof — the substrate Sandwich's not_sublist_sandwich discharges both the [h, ℓ, h] and the new [h, h, h] non-subsequence claims uniformly.

Alphabet: LugandaTone reused per Lambert's unified ℓ/h notation across §5.

Disclaimer (Lambert §5.2): [Din06] assumes maximally quadrisyllabic domains with significant compounding; that finite-domain restriction would make Prinmi co/finite (a stronger classification). The PT_3-and-not-BTLI result formalised here applies to the unbounded analysis Lambert presents; the bounded analysis is out of scope.

def Lambert2026.prinmiPred (w : List LugandaTone) : Prop

The Prinmi pitch-accent predicate [Lam26] (39):

• [h] <+ w — at least one high tone (obligatoriness).
• ¬ [h, ℓ, h] <+ w — at most one high span.
• ¬ [h, h, h] <+ w — high span length ≤ 2 syllables.

Equations

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

def Lambert2026.prinmiLang : Language LugandaTone

The Prinmi pitch-accent language.

Equations

• Lambert2026.prinmiLang = {w : List Lambert2026.LugandaTone | Lambert2026.prinmiPred w}

@[simp]

theorem Lambert2026.mem_prinmiLang (w : List LugandaTone) : w ∈ prinmiLang ↔ prinmiPred w

Membership in prinmiLang is membership in prinmiPred.

theorem Lambert2026.prinmi_isPT : prinmiLang.IsPiecewiseTestable 3

Prinmi pitch-accent ∈ PT_3 (Lambert 2026 (39)). All three conjuncts depend only on length-≤-3 subsequence presence: the length-1 [h] and the two length-3 patterns.

theorem Lambert2026.prinmi_not_isBTLI (k : ℕ) : ¬Language.IsBTLI k prinmiLang

Prinmi pitch-accent ∉ BTLI (Lambert 2026 §5.2). Same witnesses and tier-affix proof as Luganda §5.1 — Lambert: "The same words witness this nonmembership as for high-tone plateauing."

Lambert 2026 §5.3 ([Don97]): Arigibi (Trans-New Guinea) allows at most one mora with high tone (position lexically specified; words with no high tone are allowed). The phonotactic constraint is ¬h..h — no [high, high] subsequence anywhere.

Lambert: "exactly analogous to culminativity in isolation, and as such it is piecewise testable and tier-based co/finite, as demonstrated in §2.3" (Lambert's §2.3 is unbounded culminativity).

def Lambert2026.isLugHigh : LugandaTone → Bool

Boolean tier predicate selecting LugandaTone.high. Shared by §8 Arigibi and §9 Chuave.

Equations

• Lambert2026.isLugHigh Lambert2026.LugandaTone.high = true
• Lambert2026.isLugHigh Lambert2026.LugandaTone.low = false

def Lambert2026.arigibiLang : Language LugandaTone

The Arigibi pitch-accent language: at most one high mora.

Equations

• Lambert2026.arigibiLang = {w : List Lambert2026.LugandaTone | ¬[Lambert2026.LugandaTone.high, Lambert2026.LugandaTone.high].Sublist w}

@[simp]

theorem Lambert2026.mem_arigibiLang (w : List LugandaTone) : w ∈ arigibiLang ↔ ¬[LugandaTone.high, LugandaTone.high].Sublist w

Membership in arigibiLang is ¬ [h, h] <+ w.

theorem Lambert2026.arigibi_isPT : arigibiLang.IsPiecewiseTestable 2

Arigibi pitch-accent ∈ PT_2 (Lambert 2026 §5.3, formula ¬h..h). The constraint depends only on length-2 subseq [h, h].

theorem Lambert2026.arigibi_isBTN : arigibiLang.IsBTN

Arigibi pitch-accent ∈ BTN (Lambert 2026 §5.3). On the high tier, the projection has length ≤ 1, i.e., is either [] or [high] — a finite set, hence co/finite.

Lambert 2026 §5.5 ([Don97]): Chuave (Trans-New Guinea) exhibits obligatoriness — every word must contain at least one high-tone mora. There is no restriction on placement; multiple high spans are allowed. The phonotactic constraint is the simplest possible: the formula h (at least one high). This is both:

• PT_1: the constraint depends only on the length-1 subsequence [h].
• BTN (multitier finite-or-cofinite): on the high tier, the projection must be non-empty. The non-empty list set is co/finite (its complement is the singleton {[]}).

def Lambert2026.chuaveLang : Language LugandaTone

The Chuave obligatoriness language: at least one mora has high tone.

Equations

• Lambert2026.chuaveLang = {w : List Lambert2026.LugandaTone | Lambert2026.LugandaTone.high ∈ w}

@[simp]

theorem Lambert2026.mem_chuaveLang (w : List LugandaTone) : w ∈ chuaveLang ↔ LugandaTone.high ∈ w

Membership in chuaveLang is high ∈ w.

theorem Lambert2026.chuave_isPT : chuaveLang.IsPiecewiseTestable 1

Chuave obligatoriness ∈ PT_1 (Lambert 2026 §5.5). The constraint high ∈ w is the singleton subseq presence [high] <+ w.

theorem Lambert2026.chuave_isBTN : chuaveLang.IsBTN

Chuave obligatoriness ∈ BTN (Lambert 2026 §5.5, formula ¬ [⋊⋉]_{h}). On the high tier isLugHigh, the projection w.filter isLugHigh is non-empty iff high ∈ w. The non-empty set {xs | xs ≠ []} is co/finite (complement is {[]}).

Lambert 2026 §5.4 ([Kaw15], [haraguchi-1977]): Kagoshima Japanese has a pitch-accent system with exactly one high tone per word, appearing on the final or penultimate mora.

Lambert formula (42), order-based PT_3:

• h — at least one high tone (obligatoriness)
• ¬h..h — no two highs (culminativity)
• ¬h..ℓ..ℓ — high doesn't have two lows after (forces final/penult position)

Lambert formula (43), tier-based multitier definite:

• [⋊h⋉]_{h} — high tier projection equals exactly [h]
• (hℓ⋉ ∨ h⋉) — word ends with [h, ℓ] or [h]

The PT_3 result is direct from subseqSet_eq_iff. The multitier characterization uses tierEqualLang isLugHigh [.high] (high tier = singleton [h]) intersected with the disjunction of two endsWithLang cases. The §4 helpers (startsWithLang, endsWithLang, tierEqualLang) were generalized to α : Type* for this section so they apply at type LugandaTone without duplication.

We prove kagoshima_multitier_isBTLI (multitier generalized definite, k = 2). Lambert states the stronger BTD₂ classification (multitier definite — right-edge-only); BTD substrate for endsWithLang is queued for follow-up. The order/tier formulation equivalence (formulas 42 ↔ 43) is stated as a TODO theorem kagoshima_lang_eq_mt.

Alphabet: LugandaTone reused per Lambert's unified ℓ/h notation across §5.

def Lambert2026.kagoshimaPred (w : List LugandaTone) : Prop

The Kagoshima Japanese pitch-accent predicate [Lam26] (42): at least one high, no two highs, no [h, ℓ, ℓ] subseq.

Equations

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

def Lambert2026.kagoshimaLang : Language LugandaTone

The Kagoshima Japanese pitch-accent language.

Equations

• Lambert2026.kagoshimaLang = {w : List Lambert2026.LugandaTone | Lambert2026.kagoshimaPred w}

@[simp]

theorem Lambert2026.mem_kagoshimaLang (w : List LugandaTone) : w ∈ kagoshimaLang ↔ kagoshimaPred w

Membership in kagoshimaLang is membership in kagoshimaPred.

theorem Lambert2026.kagoshima_isPT : kagoshimaLang.IsPiecewiseTestable 3

Kagoshima Japanese pitch-accent ∈ PT_3 (Lambert 2026 (42)). All three conjuncts depend only on length-≤-3 subseq presence: length-1 [h], length-2 [h, h], length-3 [h, ℓ, ℓ].

def Lambert2026.kagoshimaMTLang : Language LugandaTone

The Kagoshima multitier-encoded language: high-tier-projection equals exactly [h] AND word ends with [h, ℓ] or [h]. Lambert 2026 (43).

Equations

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

theorem Lambert2026.kagoshima_multitier_isBTLI : Language.IsBTLI 2 kagoshimaMTLang

Kagoshima multitier characterization ∈ BTLI₂ (Lambert 2026 (43)). Each component lifts to IsBTLI 2:

• tierEqualLang isLugHigh [.high] via tierEqualLang_isTierBased (k = 2 > 1 = |xs|);
• endsWithLang [.high, .low] via endsWithLang_isGenDef (k = 2 ≥ 2);
• endsWithLang [.high] via endsWithLang_isGenDef (k = 2 ≥ 1). The conjunction/disjunction are closed by BoolClosure.inter / BoolClosure.union. Lambert's stronger BTD₂ classification is queued for follow-up.

Equivalence (formula 42 ↔ 43) is queued for follow-up. Lambert states the order-based predicate kagoshimaLang and the multitier predicate kagoshimaMTLang describe the same language, but the proof requires structural reasoning about how "no [h, ℓ, ℓ] subseq" combined with "exactly one high" forces the unique high to lie in the final two positions. Both formulations are independently classified above (PT_3 and BTLI_2 respectively).

Audit-flagged cross-framework engagement points. These are stated here so the disagreements (and convergences) with sibling linglib formalizations are visible rather than buried.

Each is tagged with the auditor file path it cross-references. The proofs are deferred — typically to a follow-up substrate PR (e.g. OTBound.lean) or to the chronologically-later sibling study.

theorem Lambert2026.btd_supersedes_ss_mtsl_on_uyghur : True

Lambert 2026 multitier classification structurally weaker than SS-MTSL (de Santo & Graf 2019) on Uyghur: every BTD language admits an SS-MTSL acceptor, but BTD is strictly more powerful as a phonotactic classifier — Uyghur backness harmony is BTD but [MM18] shows it is not SS-MTSL. (Stated as TODO; activates when SS-MTSL substrate lands in linglib.)

theorem Lambert2026.lambert_string_input_loses_tone_associations : True

String-input information loss for autosegmental tone analyses: two distinct autosegmental representations (e.g. multiply-linked vs. singly- linked-with-spread on a tone tier) can have the same surface string. The BTC classification of a string language therefore is not a faithful summary of an autosegmental analysis of the same surface tone pattern. Cross-references Phonology/Autosegmental/RegisterTier.lean, GrammaticalTone.lean, and Studies/Lionnet2025.lean.