@cite{lambert-2026}: 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 @cite{de-santo-graf-2019}, settling (categorically) the challenge raised by @cite{mayer-major-2018}.
• 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 @cite{jardine-2020}.

The propositional logic is BoolClosure (IsTierBased 𝒞) for 𝒞 in {IsDefinite k, IsGeneralizedDefinite k, IsStrictlyLocal k, IsStrictlyPiecewise k, IsFiniteOrCofinite}; the algebraic side is the syntactic-semigroup characterization of each class via Eilenberg @cite{eilenberg-1976} variety equations (e.g., D = ⟦sx̄ = x̄⟧, ℒℐ = ⟦x^ω y x^ω z x^ω = x^ω y x^ω⟧ per @cite{straubing-1985} and @cite{almeida-1995}). The Lean substrate (BoolClosure, IsBTC, IsTierBased) lives in Subregular/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 @cite{mayer-major-2018}'s categorical idealization, and a separate literature line — @cite{mccollum-2019} — 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)). @cite{jardine-2020}'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 NamedConstraint 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 Theories/Phonology/Subregular/OTBound.lean.
• Harmonic Serialism: Phenomena/Tone/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 Theories/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: Theories/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 @cite{de-santo-graf-2019}: 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.

inductive Phenomena.Phonotactics.Studies.Lambert2026.IbanSyl : Type

Iban syllable type @cite{omar-1969}: stressed (σ́) or unstressed (σ). The two-letter alphabet of Lambert (2026) §2.1.

• unstressed : IbanSyl
• stressed : IbanSyl

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instDecidableEqIbanSyl : DecidableEq IbanSyl

Equations

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

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instReprIbanSyl : Repr IbanSyl

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.instReprIbanSyl = { reprPrec := Phenomena.Phonotactics.Studies.Lambert2026.instReprIbanSyl.repr }

def Phenomena.Phonotactics.Studies.Lambert2026.instReprIbanSyl.repr : IbanSyl → ℕ → Std.Format

Equations

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

def Phenomena.Phonotactics.Studies.Lambert2026.ibanGrammar : Core.Computability.Subregular.DefiniteGrammar 1 IbanSyl

The Iban stress-final language: a word is well-formed iff its final syllable is stressed @cite{omar-1969}. As a DefiniteGrammar 1: the permitted length-1 right-edge substring is [stressed].

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.ibanGrammar = { permitted := {[Phenomena.Phonotactics.Studies.Lambert2026.IbanSyl.stressed]} }

def Phenomena.Phonotactics.Studies.Lambert2026.ibanLang : Language IbanSyl

The Iban stress-final language as a Language IbanSyl.

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.ibanLang = Core.Computability.Subregular.EdgeDefiniteGrammar.lang Phenomena.Phonotactics.Studies.Lambert2026.ibanGrammar

theorem Phenomena.Phonotactics.Studies.Lambert2026.iban_isDefinite_one : Core.Computability.Subregular.IsDefinite 1 ibanLang

Iban stress-final ∈ D_1 (Lambert 2026 §2.1, paper p. 4 example (2)). Definitional witness: the DefiniteGrammar 1 whose permitted final 1-suffix is [stressed]. The general k-definite Proposition (4) characterizes this class abstractly; the Iban witness is the specialisation for k = 1.

def Phenomena.Phonotactics.Studies.Lambert2026.amaraGrammar : Core.Computability.Subregular.DefiniteGrammar 2 IbanSyl

Amara stress @cite{thurston-1966}: penultimate-syllable stress with the monosyllabic exception (single syllable bears stress).

Equations

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

def Phenomena.Phonotactics.Studies.Lambert2026.amaraLang : Language IbanSyl

The Amara stress-penult language.

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.amaraLang = Core.Computability.Subregular.EdgeDefiniteGrammar.lang Phenomena.Phonotactics.Studies.Lambert2026.amaraGrammar

theorem Phenomena.Phonotactics.Studies.Lambert2026.amara_isDefinite_two : Core.Computability.Subregular.IsDefinite 2 amaraLang

Amara stress-penult ∈ D_2 (Lambert 2026 §2.1). Witnessed by the 2-grammar permitting either a stressed monosyllable or a stressed-then- unstressed 2-suffix.

def Phenomena.Phonotactics.Studies.Lambert2026.finnishGrammar : Core.Computability.Subregular.ReverseDefiniteGrammar 1 IbanSyl

Finnish stress @cite{suomi-toivanen-ylitalo-2008}: primary stress is fixed to the initial syllable. The reverse-definite dual of Iban stress-final, witnessing the IsReverseDefinite 1 class @cite{lambert-2026} §2.2.

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.finnishGrammar = { permitted := {[Phenomena.Phonotactics.Studies.Lambert2026.IbanSyl.stressed]} }

def Phenomena.Phonotactics.Studies.Lambert2026.finnishLang : Language IbanSyl

The Finnish stress-initial language.

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.finnishLang = Core.Computability.Subregular.EdgeDefiniteGrammar.lang Phenomena.Phonotactics.Studies.Lambert2026.finnishGrammar

theorem Phenomena.Phonotactics.Studies.Lambert2026.finnish_isReverseDefinite_one : Core.Computability.Subregular.IsReverseDefinite 1 finnishLang

Finnish stress-initial ∈ K_1 (Lambert 2026 §2.2, paper p. 5 example (6)). Definitional witness: the ReverseDefiniteGrammar 1 whose permitted initial 1-prefix is [stressed].

inductive Phenomena.Phonotactics.Studies.Lambert2026.UyghurSeg : Type

Uyghur segment classes relevant to backness harmony @cite{mayer-major-2018} @cite{lambert-2026} (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 Phenomena.Phonotactics.Studies.Lambert2026.instDecidableEqUyghurSeg : DecidableEq UyghurSeg

Equations

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

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instReprUyghurSeg : Repr UyghurSeg

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.instReprUyghurSeg = { reprPrec := Phenomena.Phonotactics.Studies.Lambert2026.instReprUyghurSeg.repr }

def Phenomena.Phonotactics.Studies.Lambert2026.instReprUyghurSeg.repr : UyghurSeg → ℕ → Std.Format

Equations

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

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 Phenomena.Phonotactics.Studies.Lambert2026.isHarmonyingVowel : UyghurSeg → Bool

Harmonising-vowel tier: V_f ∪ V_b.

Equations

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

def Phenomena.Phonotactics.Studies.Lambert2026.isDorsal : UyghurSeg → Bool

Dorsal-consonant tier: C_f ∪ C_b.

Equations

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

def Phenomena.Phonotactics.Studies.Lambert2026.isSuffixFront : UyghurSeg → Bool

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

Equations

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

def Phenomena.Phonotactics.Studies.Lambert2026.isSuffixBack : UyghurSeg → Bool

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

Equations

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

Atomic tier-projected definite languages

Each of the four atomic predicates in (35) is a IsTierBased (IsDefinite 1) test. We build them as DefiniteGrammar 1 instances on the filtered tier and lift via IsTierBased.

def Phenomena.Phonotactics.Studies.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

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

def Phenomena.Phonotactics.Studies.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

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.tierEmptyLang_isTierBased (T : UyghurSeg → Bool) : Core.Computability.Subregular.IsTierBased (Core.Computability.Subregular.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 Phenomena.Phonotactics.Studies.Lambert2026.tierEndsWithLang_isTierBased (T : UyghurSeg → Bool) (x : UyghurSeg) : Core.Computability.Subregular.IsTierBased (Core.Computability.Subregular.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 Phenomena.Phonotactics.Studies.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 @cite{mccollum-2019} gradience disclaimer.

Equations

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.uyghur_backness_isBTD : ∃ (k : ℕ), Core.Computability.Subregular.IsBTD k uyghurBacknessLang

Uyghur backness harmony ∈ BTD₁ (Lambert 2026 §4.3, eq. (35), refining @cite{mayer-major-2018}). 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 BoolClosure.{base, compl, union, inter} applied to the four atomic tier-projected definite languages.

inductive Phenomena.Phonotactics.Studies.Lambert2026.KShoTone : Type

Karanga Shona tone alphabet @cite{odden-1984} @cite{lambert-2026} §5.6: low (ℓ) and high (h).

• low : KShoTone
• high : KShoTone

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instDecidableEqKShoTone : DecidableEq KShoTone

Equations

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

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instReprKShoTone : Repr KShoTone

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.instReprKShoTone = { reprPrec := Phenomena.Phonotactics.Studies.Lambert2026.instReprKShoTone.repr }

def Phenomena.Phonotactics.Studies.Lambert2026.instReprKShoTone.repr : KShoTone → ℕ → Std.Format

Equations

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

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 Phenomena.Phonotactics.Studies.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

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

def Phenomena.Phonotactics.Studies.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

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

def Phenomena.Phonotactics.Studies.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

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

def Phenomena.Phonotactics.Studies.Lambert2026.isHigh : KShoTone → Bool

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

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.isHigh Phenomena.Phonotactics.Studies.Lambert2026.KShoTone.high = true
• Phenomena.Phonotactics.Studies.Lambert2026.isHigh Phenomena.Phonotactics.Studies.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 Phenomena.Phonotactics.Studies.Lambert2026.startsWithLang_isGenDef {α : Type u_1} (xs : List α) (k : ℕ) (hk : xs.length ≤ k) : Core.Computability.Subregular.IsGeneralizedDefinite k (startsWithLang xs)

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 Phenomena.Phonotactics.Studies.Lambert2026.endsWithLang_isGenDef {α : Type u_1} (xs : List α) (k : ℕ) (hk : xs.length ≤ k) : Core.Computability.Subregular.IsGeneralizedDefinite k (endsWithLang xs)

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 Phenomena.Phonotactics.Studies.Lambert2026.tierEqualLang_isTierBased {α : Type u_1} (T : α → Bool) (xs : List α) (k : ℕ) (hk : xs.length < k) : Core.Computability.Subregular.IsTierBased (Core.Computability.Subregular.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 Phenomena.Phonotactics.Studies.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 Phenomena.Phonotactics.Studies.Lambert2026.phi_F : Language KShoTone

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

Equations

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.phi_F_isGenDef : Core.Computability.Subregular.IsGeneralizedDefinite 5 phi_F

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 Phenomena.Phonotactics.Studies.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 Phenomena.Phonotactics.Studies.Lambert2026.karanga_shona_verb_stem_isBTLI : ∃ (k : ℕ), Core.Computability.Subregular.IsBTLI k karangaShonaVerbStemLang

Karanga Shona verb-stem tone ∈ BTLI₅ (Lambert 2026 §5.6, refining @cite{jardine-2020}). 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 + BoolClosure.base; the disjunction is closed by BoolClosure.union.

@[reducible, inline]

abbrev Phenomena.Phonotactics.Studies.Lambert2026.TsuutinaSeg : Type

The Tsuut'ina sibilant alphabet @cite{cook-1978} is the shared three-class SibilantTierSeg (anterior s, posterior ʃ, neutral non-sibilant) defined in Theories/Phonology/SibilantTier.lean.

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.TsuutinaSeg = Theories.Phonology.SibilantTier.SibilantTierSeg

def Phenomena.Phonotactics.Studies.Lambert2026.tsuutinaTSLGrammar : Core.Computability.Subregular.TSLGrammar 2 TsuutinaSeg

The TSL_2 grammar for Tsuut'ina asymmetric sibilant harmony @cite{cook-1978} @cite{lambert-2026} §4.2: anterior preceding posterior on the sibilant tier is forbidden. Reuses the shared substrate asymmetricHarmonyAntFirst from Theories/Phonology/SibilantTier.lean.

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.tsuutinaTSLGrammar = Theories.Phonology.SibilantTier.asymmetricHarmonyAntFirst

def Phenomena.Phonotactics.Studies.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

• Phenomena.Phonotactics.Studies.Lambert2026.tsuutinaLang = Phenomena.Phonotactics.Studies.Lambert2026.tsuutinaTSLGrammar.lang

theorem Phenomena.Phonotactics.Studies.Lambert2026.tsuutina_isTSL2 : Core.Computability.Subregular.IsTierStrictlyLocal 2 tsuutinaLang

Tsuut'ina asymmetric harmony ∈ TSL_2 (Lambert 2026 §4.2). Definitional witness: the TSL_2 grammar tsuutinaTSLGrammar.

Refutation: Tsuut'ina ∉ BTLI

Lambert (2026) §4.2 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 substrate Sandwich (in Core/Computability/Subregular/Sandwich.lean) handles 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 Phenomena.Phonotactics.Studies.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

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

@[reducible, inline]

abbrev Phenomena.Phonotactics.Studies.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

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.tsuutina_not_isBTLI (k : ℕ) : ¬Core.Computability.Subregular.IsBTLI k tsuutinaLang

Tsuut'ina asymmetric harmony ∉ BTLI (Lambert 2026 §4.2, parametrised counterexample).

inductive Phenomena.Phonotactics.Studies.Lambert2026.LugandaTone : Type

Luganda tone alphabet @cite{hyman-katamba-2010}: low (ℓ) and high (h), following @cite{jardine-2020}'s identification of "intermediate" with low in the input.

• low : LugandaTone
• high : LugandaTone

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instDecidableEqLugandaTone : DecidableEq LugandaTone

Equations

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

@[implicit_reducible]

instance Phenomena.Phonotactics.Studies.Lambert2026.instReprLugandaTone : Repr LugandaTone

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.instReprLugandaTone = { reprPrec := Phenomena.Phonotactics.Studies.Lambert2026.instReprLugandaTone.repr }

def Phenomena.Phonotactics.Studies.Lambert2026.instReprLugandaTone.repr : LugandaTone → ℕ → Std.Format

Equations

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

def Phenomena.Phonotactics.Studies.Lambert2026.lugandaPred (w : List LugandaTone) : Prop

The Luganda high-tone plateauing predicate @cite{lambert-2026} (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 Phenomena.Phonotactics.Studies.Lambert2026.lugandaLang : Language LugandaTone

The Luganda high-tone plateauing language.

Equations

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

@[simp]

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

Membership in lugandaLang is membership in lugandaPred.

theorem Phenomena.Phonotactics.Studies.Lambert2026.luganda_isPT : Core.Computability.Subregular.IsPiecewiseTestable 3 lugandaLang

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 substrate Sandwich (in Core/Computability/Subregular/Sandwich.lean) handles 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 Phenomena.Phonotactics.Studies.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 Phenomena.Phonotactics.Studies.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 Phenomena.Phonotactics.Studies.Lambert2026.luganda_not_isBTLI (k : ℕ) : ¬Core.Computability.Subregular.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 (@cite{ding-2006}): 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): @cite{ding-2006} 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 Phenomena.Phonotactics.Studies.Lambert2026.prinmiPred (w : List LugandaTone) : Prop

The Prinmi pitch-accent predicate @cite{lambert-2026} (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 Phenomena.Phonotactics.Studies.Lambert2026.prinmiLang : Language LugandaTone

The Prinmi pitch-accent language.

Equations

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

@[simp]

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

Membership in prinmiLang is membership in prinmiPred.

theorem Phenomena.Phonotactics.Studies.Lambert2026.prinmi_isPT : Core.Computability.Subregular.IsPiecewiseTestable 3 prinmiLang

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 Phenomena.Phonotactics.Studies.Lambert2026.prinmi_not_isBTLI (k : ℕ) : ¬Core.Computability.Subregular.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 (@cite{donohue-1997}): 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 Phenomena.Phonotactics.Studies.Lambert2026.isLugHigh : LugandaTone → Bool

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

Equations

• Phenomena.Phonotactics.Studies.Lambert2026.isLugHigh Phenomena.Phonotactics.Studies.Lambert2026.LugandaTone.high = true
• Phenomena.Phonotactics.Studies.Lambert2026.isLugHigh Phenomena.Phonotactics.Studies.Lambert2026.LugandaTone.low = false

def Phenomena.Phonotactics.Studies.Lambert2026.arigibiLang : Language LugandaTone

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

Equations

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

@[simp]

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

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.arigibi_isPT : Core.Computability.Subregular.IsPiecewiseTestable 2 arigibiLang

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.arigibi_isBTN : Core.Computability.Subregular.IsBTN arigibiLang

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 (@cite{donohue-1997}): 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 Phenomena.Phonotactics.Studies.Lambert2026.chuaveLang : Language LugandaTone

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

Equations

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

@[simp]

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

Membership in chuaveLang is high ∈ w.

theorem Phenomena.Phonotactics.Studies.Lambert2026.chuave_isPT : Core.Computability.Subregular.IsPiecewiseTestable 1 chuaveLang

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

theorem Phenomena.Phonotactics.Studies.Lambert2026.chuave_isBTN : Core.Computability.Subregular.IsBTN chuaveLang

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 (@cite{kawahara-2015}, @cite{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 Phenomena.Phonotactics.Studies.Lambert2026.kagoshimaPred (w : List LugandaTone) : Prop

The Kagoshima Japanese pitch-accent predicate @cite{lambert-2026} (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 Phenomena.Phonotactics.Studies.Lambert2026.kagoshimaLang : Language LugandaTone

The Kagoshima Japanese pitch-accent language.

Equations

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

@[simp]

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

Membership in kagoshimaLang is membership in kagoshimaPred.

theorem Phenomena.Phonotactics.Studies.Lambert2026.kagoshima_isPT : Core.Computability.Subregular.IsPiecewiseTestable 3 kagoshimaLang

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 Phenomena.Phonotactics.Studies.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 Phenomena.Phonotactics.Studies.Lambert2026.kagoshima_multitier_isBTLI : Core.Computability.Subregular.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 Phenomena.Phonotactics.Studies.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 @cite{mayer-major-2018} shows it is not SS-MTSL. (Stated as TODO; activates when SS-MTSL substrate lands in linglib.)

theorem Phenomena.Phonotactics.Studies.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 Theories/Phonology/Autosegmental/RegisterTier.lean, GrammaticalTone.lean, and Phenomena/Tone/Studies/Lionnet2025.lean.