Lambert (2026): Multitier phonotactics with logic and algebra

This file formalizes the paper's classifications: attested constraints on stress, harmony, and tone are placed in the multitier extensions of the definite, reverse definite, generalized definite, and co/finite classes, the Boolean closures of the tier-projected classes, by writing each constraint as a propositional formula over tier affixes, and are refuted from a class by a pair of words the class cannot separate. With the tier literals Language.tierWord, tierPrefix, and tierSuffix, a membership proof has the shape of its formula: the bounded stress patterns with culminativity are multitier definite or reverse definite, the four unbounded patterns of Hayes's typology are multitier reverse definite, definite, or generalized definite as their defaults demand, Uyghur backness harmony is multitier definite (uyghur_isBTD), and the Karanga Shona verb stem is multitier generalized definite (karangaShona_isBTLI). The refutations follow the paper's parameterized witnesses: culminativity alone is not generalized definite, culminative stress-final is not definite, and Tsuut'ina sibilant harmony, Luganda plateauing, and Prinmi are not multitier generalized definite (tsuutina_not_isBTLI, luganda_not_isBTLI). Luganda's plateauing conjunct holds of exactly the outputs of Hyman and Katamba's plateauing map (plateauing_iff_mem_range_utp). Following §6, stress-initial is refuted from the definite class, stress-penult from the reverse definite class, and culminative stress-penult from the generalized definite class by an idempotent syntactic class that fails the class's equation (finnish_not_isDefinite, amara_not_isReverseDefinite, stressPenultCulminative_not_isGeneralizedDefinite), and culminative stress-penult from the multitier reverse definite class by the equation of (62) (stressPenultCulminative_not_isBTK).

Implementation notes

Patterns are string languages over the paper's alphabets: syllables by stress, and by weight and stress for unbounded stress; the sibilant classes, which are the classes Hansson's segments project to, none off the tier; segment classes for Uyghur, with suffix material marked as such following the paper; and two tones, without tone associations. A pattern is defined by one of the paper's formulae, and where the paper gives an order-based and a tier-based formula for the same pattern both are classified but their equivalence is proved only for Navajo and Chuave. Windows are the paper's: the length of the longest affix, and one more for a whole tier word, whose boundary markers count. The Uyghur pattern is the categorical one of Mayer and Major that the paper analyzes.

TODO

Prove the equivalence of the order-based and tier-based formulae for Kagoshima Japanese ((42), (43)) and for Karanga Shona ((46)–(49)), and the piecewise testability of the Tsuut'ina grammar. The description of the Karanga Shona stem by substrings ((50)), which makes it locally testable, are not formalized. Of the equations for the multitier classes ((60)–(63), Table 6), only (62) is proved (Language.exists_isBTK_iff).

References

• [Lam26]
• [Oma69], [Thu66], [STY08]
• [Hay95b], [Rob87a], [BB70], [Gru69], [Kru61]
• [Hei10], [SH67], [Coo78], [MM18], [Han10]
• [HK10], [Din06], [Don97], [Odd84], [Jar20]

Bookended witnesses

The paper's parameterized witnesses are words aᵏ ++ mid ++ bᵏ.

Bounded stress (§2)

Stress-final, stress-penult, and stress-initial are definite, definite, and reverse definite ((2), (5), (6)). Culminativity, at most one primary stress, is tier-based co/finite on the stress tier but not generalized definite, so it lifts each bounded pattern out of the affix classes to the multitier ones ((13)); with it stress-final is no longer definite (§2.3).

inductive Lambert2026.Syl : Type

A syllable, unstressed or bearing primary stress.

• unstressed : Syl
• stressed : Syl

@[instance_reducible]

instance Lambert2026.instDecidableEqSyl : DecidableEq Syl

Equations

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

@[instance_reducible]

instance Lambert2026.instFintypeSyl : Fintype Syl

Equations

• Lambert2026.instFintypeSyl = { elems := { val := ↑Lambert2026.Syl.enumList, nodup := Lambert2026.Syl.enumList_nodup }, complete := Lambert2026.instFintypeSyl._proof_1 }

@[instance_reducible]

instance Lambert2026.instReprSyl : Repr Syl

Equations

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

def Lambert2026.instReprSyl.repr : Syl → ℕ → Std.Format

Equations

• Lambert2026.instReprSyl.repr Lambert2026.Syl.unstressed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lambert2026.Syl.unstressed")).group prec✝
• Lambert2026.instReprSyl.repr Lambert2026.Syl.stressed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lambert2026.Syl.stressed")).group prec✝

def Lambert2026.Syl.isStressed : Syl → Bool

The stress tier.

Equations

• Lambert2026.Syl.stressed.isStressed = true
• Lambert2026.Syl.unstressed.isStressed = false

def Lambert2026.iban : Language Syl

Iban stresses the final syllable ((2), [Oma69]), σ́⋉.

Equations

• Lambert2026.iban = Language.ofSuffix [Lambert2026.Syl.stressed]

theorem Lambert2026.iban_isDefinite : iban.IsDefinite 1

def Lambert2026.amara : Language Syl

Amara stresses the penult ((5), [Thu66]), σ́Σ⋉ ∨ ⋊σ́⋉.

Equations

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

@[simp]

theorem Lambert2026.mem_amara {w : List Syl} : w ∈ amara ↔ Edge.right.takeAt 2 w ∈ {[Syl.stressed], [Syl.stressed, Syl.unstressed], [Syl.stressed, Syl.stressed]}

theorem Lambert2026.amara_isDefinite : amara.IsDefinite 2

def Lambert2026.finnish : Language Syl

Finnish stresses the initial syllable ((6), [STY08]), ⋊σ́.

Equations

• Lambert2026.finnish = Language.ofPrefix [Lambert2026.Syl.stressed]

theorem Lambert2026.finnish_isReverseDefinite : finnish.IsReverseDefinite 1

def Lambert2026.culminativity : Language Syl

Culminativity (§2.3) allows at most one stressed syllable, [⋊⋉ ∨ ⋊σ́⋉]_{σ́}.

Equations

• Lambert2026.culminativity = {w : List Lambert2026.Syl | List.filter Lambert2026.Syl.isStressed w = [] ∨ List.filter Lambert2026.Syl.isStressed w = [Lambert2026.Syl.stressed]}

theorem Lambert2026.culminativity_isTierBased : Language.IsTierBased Language.IsFiniteOrCofinite culminativity

Culminativity is tier-based co/finite, since on the stress tier the word is empty or a single stressed syllable.

theorem Lambert2026.culminativity_not_isGeneralizedDefinite (k : ℕ) : ¬culminativity.IsGeneralizedDefinite k

Culminativity is not generalized definite, since σᵏσ́σᵏ is in and σᵏσ́σ́σᵏ is out with the same prefix and suffix of length k.

def Lambert2026.stressFinalCulminative : Language Syl

Culminative stress-final ((13a)) is σ́⋉ ∧ [⋊σ́⋉]_{σ́}.

Equations

• Lambert2026.stressFinalCulminative = Lambert2026.iban ⊓ Language.tierWord Lambert2026.Syl.isStressed [Lambert2026.Syl.stressed]

theorem Lambert2026.stressFinalCulminative_isBTD : Language.IsBTD 2 stressFinalCulminative

def Lambert2026.stressPenultCulminative : Language Syl

Culminative stress-penult ((13b)) is (σ́σ⋉ ∨ ⋊σ́⋉) ∧ [⋊σ́⋉]_{σ́}.

Equations

• Lambert2026.stressPenultCulminative = Lambert2026.amara ⊓ Language.tierWord Lambert2026.Syl.isStressed [Lambert2026.Syl.stressed]

theorem Lambert2026.stressPenultCulminative_isBTD : Language.IsBTD 2 stressPenultCulminative

def Lambert2026.stressInitialCulminative : Language Syl

Culminative stress-initial ((13c)) is ⋊σ́ ∧ [⋊σ́⋉]_{σ́}.

Equations

• Lambert2026.stressInitialCulminative = Lambert2026.finnish ⊓ Language.tierWord Lambert2026.Syl.isStressed [Lambert2026.Syl.stressed]

theorem Lambert2026.stressInitialCulminative_isBTK : Language.IsBTK 2 stressInitialCulminative

theorem Lambert2026.stressFinalCulminative_not_isDefinite (k : ℕ) : ¬stressFinalCulminative.IsDefinite k

Culminative stress-final is not definite (§2.3), since σσᵏσ́ is in and σ́σᵏσ́ is out with the same suffix of length k; strict locality is more powerful than definiteness.

Unbounded stress (§3)

The four patterns of Hayes's typology ([Hay95b]) over syllables distinguished by weight: the default-to-same patterns are multitier reverse definite or definite, the default-to-opposite ones multitier generalized definite ((20), (23), (26), (29)).

inductive Lambert2026.QSyl : Type

A syllable by weight and stress.

• light : QSyl
• heavy : QSyl
• lightStressed : QSyl
• heavyStressed : QSyl

@[instance_reducible]

instance Lambert2026.instDecidableEqQSyl : DecidableEq QSyl

Equations

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

@[instance_reducible]

instance Lambert2026.instReprQSyl : Repr QSyl

Equations

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

def Lambert2026.instReprQSyl.repr : QSyl → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Lambert2026.instReprQSyl.repr Lambert2026.QSyl.light prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lambert2026.QSyl.light")).group prec✝
• Lambert2026.instReprQSyl.repr Lambert2026.QSyl.heavy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lambert2026.QSyl.heavy")).group prec✝

def Lambert2026.QSyl.isStressed : QSyl → Bool

The stress tier.

Equations

• Lambert2026.QSyl.lightStressed.isStressed = true
• Lambert2026.QSyl.heavyStressed.isStressed = true
• x✝.isStressed = false

def Lambert2026.QSyl.isHeavy : QSyl → Bool

The heavy tier.

Equations

• Lambert2026.QSyl.heavy.isHeavy = true
• Lambert2026.QSyl.heavyStressed.isHeavy = true
• x✝.isHeavy = false

def Lambert2026.oneStress : Language QSyl

A word has exactly one primary stress, [⋊σ́⋉]_{σ́}.

Equations

• Lambert2026.oneStress = Language.tierWord Lambert2026.QSyl.isStressed [Lambert2026.QSyl.lightStressed] ⊔ Language.tierWord Lambert2026.QSyl.isStressed [Lambert2026.QSyl.heavyStressed]

theorem Lambert2026.oneStress_isBTD : Language.IsBTD 2 oneStress

theorem Lambert2026.oneStress_isBTK : Language.IsBTK 2 oneStress

def Lambert2026.amele : Language QSyl

Amele ((20), [Rob87a]) stresses the leftmost heavy syllable, else the leftmost.

Equations

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

theorem Lambert2026.amele_isBTK : Language.IsBTK 2 amele

def Lambert2026.golin : Language QSyl

Golin ((23), [BB70]) stresses the rightmost heavy syllable, else the rightmost.

Equations

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

theorem Lambert2026.golin_isBTD : Language.IsBTD 2 golin

def Lambert2026.kwakwala : Language QSyl

Kwak'wala ((26), [Gru69]) stresses the leftmost heavy syllable, else the rightmost.

Equations

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

theorem Lambert2026.kwakwala_isBTLI : Language.IsBTLI 2 kwakwala

def Lambert2026.chuvash : Language QSyl

Chuvash ((29), [Kru61]) stresses the rightmost heavy syllable, else the leftmost.

Equations

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

theorem Lambert2026.chuvash_isBTLI : Language.IsBTLI 2 chuvash

Harmony (§4)

Navajo's symmetric sibilant harmony ([SH67]) is multitier co/finite, one of the two sibilant tiers being empty, and coincides with the tier-based agreement grammar, which the library already identifies with [Hei10]'s forbidden subsequences; read through the sibilant classes of segments, it is [Han10]'s agreement in [anterior] (preimage_sibilantClass_navajo). Tsuut'ina's asymmetric harmony ([Coo78]) is tier-based strictly local but not multitier generalized definite: an internal factor is needed. Uyghur backness harmony ([MM18]) is multitier definite, lying between the two.

def Lambert2026.isAnterior (c : Option Bool) : Bool

The alveolar tier of the sibilant classes.

Equations

• Lambert2026.isAnterior c = (c == some true)

def Lambert2026.isPosterior (c : Option Bool) : Bool

The postalveolar tier of the sibilant classes.

Equations

• Lambert2026.isPosterior c = (c == some false)

def Lambert2026.navajo : Language (Option Bool)

In Navajo ((30)) the sibilants agree, [⋊⋉]_s ∨ [⋊⋉]_ʃ.

Equations

• Lambert2026.navajo = Language.tierWord Lambert2026.isAnterior [] ⊔ Language.tierWord Lambert2026.isPosterior []

theorem Lambert2026.navajo_isBTN : navajo.IsBTN

theorem Lambert2026.navajo_eq_agree : navajo = (Subregular.TierStrictlyLocalGrammar.agree fun (x : Option Bool) => x.isSome = true).language

The tier formula for Navajo describes the agreement grammar on the sibilant tier, which is tier-based strictly local and strictly piecewise.

theorem Lambert2026.preimage_sibilantClass_navajo : List.map Hansson2010.sibilantClass ⁻¹' navajo = Hansson2010.navajoSibilantHarmony.language

The sibilant classes are the classes of Hansson's segments, and Hansson's language is the inverse image of Navajo's tier formula under the class map.

def Lambert2026.antPostForbidden (a b : Option Bool) : Prop

Alveolar immediately before postalveolar on the sibilant tier, the adjacency Tsuut'ina forbids ((31)).

Equations

• Lambert2026.antPostForbidden a b = (a = some true ∧ b = some false)

@[instance_reducible]

instance Lambert2026.instDecidableRelOptionBoolAntPostForbidden : DecidableRel antPostForbidden

Equations

• Lambert2026.instDecidableRelOptionBoolAntPostForbidden x✝¹ x✝ = { decide := decide (x✝¹ = some true) && decide (x✝ = some false), reflects_decide := ⋯ }

def Lambert2026.tsuutinaGrammar : Subregular.TierStrictlyLocalGrammar 2 (Option Bool)

In Tsuut'ina asymmetric harmony ([Coo78]) an alveolar sibilant is not followed on the tier by a postalveolar one, ¬[sʃ]_{s,ʃ}.

Equations

• Lambert2026.tsuutinaGrammar = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs Lambert2026.antPostForbidden fun (x : Option Bool) => x.isSome = true

def Lambert2026.tsuutina : Language (Option Bool)

The Tsuut'ina language.

Equations

• Lambert2026.tsuutina = Lambert2026.tsuutinaGrammar.language

theorem Lambert2026.tsuutina_isTierStrictlyLocal : Language.IsTierStrictlyLocal 2 tsuutina

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

Tsuut'ina is not multitier generalized definite (§4.2), since ʃᵏ⁺¹sᵏ⁺¹ is in and ʃᵏsʃsᵏ is out with the same affixes of length k on every tier.

inductive Lambert2026.UyghurSeg : Type

The segment classes of Uyghur backness harmony ((34)) are the harmonizing vowels and dorsal consonants, front or back, the same marked as suffix material, and the rest.

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

@[instance_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.

@[instance_reducible]

instance Lambert2026.instReprUyghurSeg : Repr UyghurSeg

Equations

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

def Lambert2026.UyghurSeg.isHarmonizingVowel : UyghurSeg → Bool

The harmonizing-vowel tier V_f ∪ V_b.

Equations

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

def Lambert2026.UyghurSeg.isDorsal : UyghurSeg → Bool

The dorsal tier C_f ∪ C_b.

Equations

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

def Lambert2026.UyghurSeg.isSuffixFront : UyghurSeg → Bool

The front-suffix tier S_f.

Equations

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

def Lambert2026.UyghurSeg.isSuffixBack : UyghurSeg → Bool

The back-suffix tier S_b.

Equations

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

def Lambert2026.uyghur : Language UyghurSeg

In Uyghur backness harmony ((35)) the suffix agrees with the rightmost harmonizing vowel, or failing that with the rightmost dorsal, each implication φ → ψ written φᶜ ⊔ ψ.

Equations

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

theorem Lambert2026.uyghur_isBTD : Language.IsBTD 1 uyghur

Uyghur backness harmony is multitier definite (§4.3), since every literal is a tier suffix.

Tone (§5)

Tone strings over low and high, without their associations to segments. Luganda plateauing and Prinmi are piecewise testable but not multitier generalized definite; Arigibi, Chuave, and Kagoshima Japanese are piecewise testable and multitier co/finite or definite; the Karanga Shona verb stem is multitier generalized definite. Order-based formulae are Boolean combinations of shuffle ideals.

inductive Lambert2026.Tone : Type

A tone.

• low : Tone
• high : Tone

@[instance_reducible]

instance Lambert2026.instDecidableEqTone : DecidableEq Tone

Equations

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

@[instance_reducible]

instance Lambert2026.instReprTone : Repr Tone

Equations

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

def Lambert2026.instReprTone.repr : Tone → ℕ → Std.Format

Equations

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

def Lambert2026.Tone.isHigh : Tone → Bool

The high-tone tier.

Equations

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

def Lambert2026.luganda : Language Tone

Luganda high-tone plateauing ((37), [HK10]) is ¬h..ℓ..h ∧ (h → h..ℓ).

Equations

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

theorem Lambert2026.luganda_isPiecewiseTestable : luganda.IsPiecewiseTestable 3

def Lambert2026.Tone.toTBU : Tone → Tone.TBU

A tone as a timing unit's association state, low read as unspecified (§5.1).

Equations

• Lambert2026.Tone.high.toTBU = Tone.TBU.H
• Lambert2026.Tone.low.toTBU = Tone.TBU.O

theorem Lambert2026.plateauing_iff_mem_range_utp (w : List Tone) : w ∉ Language.shuffleIdeal [Tone.high, Tone.low, Tone.high] ↔ List.map Tone.toTBU w ∈ Set.range Tone.utp.map

The plateauing conjunct ¬h..ℓ..h holds of exactly the outputs of Hyman and Katamba's plateauing map.

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

Luganda plateauing is not multitier generalized definite (§5.1).

def Lambert2026.prinmi : Language Tone

Prinmi ((39), [Din06]) has one high span of at most two syllables, h ∧ ¬h..ℓ..h ∧ ¬h..h..h.

Equations

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

theorem Lambert2026.prinmi_isPiecewiseTestable : prinmi.IsPiecewiseTestable 3

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

Prinmi is not multitier generalized definite (§5.2), by the Luganda witnesses.

def Lambert2026.arigibi : Language Tone

Arigibi ((40), [Don97]) has at most one high mora, ¬h..h.

Equations

• Lambert2026.arigibi = (Language.shuffleIdeal [Lambert2026.Tone.high, Lambert2026.Tone.high])ᶜ

theorem Lambert2026.arigibi_isPiecewiseTestable : arigibi.IsPiecewiseTestable 2

theorem Lambert2026.arigibi_isTierBased : Language.IsTierBased Language.IsFiniteOrCofinite arigibi

Arigibi is tier-based co/finite (§5.3), since on the high tier the word is empty or a single high, which is culminativity on tone.

def Lambert2026.kagoshima : Language Tone

Kagoshima Japanese ((42), [Din06]) has one high tone, on the final or the penultimate mora, h ∧ ¬h..h ∧ ¬h..ℓ..ℓ.

Equations

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

theorem Lambert2026.kagoshima_isPiecewiseTestable : kagoshima.IsPiecewiseTestable 3

def Lambert2026.kagoshimaTier : Language Tone

By tiers ((43)), Kagoshima Japanese is [⋊h⋉]_{h} ∧ (hℓ⋉ ∨ h⋉).

Equations

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

theorem Lambert2026.kagoshimaTier_isBTD : Language.IsBTD 2 kagoshimaTier

def Lambert2026.chuave : Language Tone

Chuave ((44), [Don97]) requires at least one high mora, h.

Equations

• Lambert2026.chuave = Language.shuffleIdeal [Lambert2026.Tone.high]

theorem Lambert2026.chuave_isPiecewiseTestable : chuave.IsPiecewiseTestable 1

theorem Lambert2026.chuave_isLocallyTestable : chuave.IsLocallyTestable 1

Chuave is also locally testable (§5.5), since a high mora anywhere in a word is a factor of it.

theorem Lambert2026.chuave_eq_compl_tierWord : chuave = (Language.tierWord Tone.isHigh [])ᶜ

Chuave is the complement of an empty high tier, ¬[⋊⋉]_{h}.

theorem Lambert2026.chuave_isBTN : chuave.IsBTN

def Lambert2026.karangaShort : Language Tone

The seven fully specified Karanga Shona stems (§5.6, [Odd84]).

Equations

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

def Lambert2026.karangaShona : Language Tone

The Karanga Shona verb stem ((48), (49)) is a short stem, a low-toned root ⋊ℓhhℓ ∧ [⋊hh⋉]_{h}, or a high-toned root ⋊hhhℓ ∧ ℓh⋉ ∧ [⋊hhhh⋉]_{h}.

Equations

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

theorem Lambert2026.karangaShona_isBTLI : Language.IsBTLI 5 karangaShona

The Karanga Shona verb stem is multitier generalized definite (§5.6, refining [Jar20]), and needs both tier prefixes and tier suffixes.

Classification through equations (§6)

The window characterizations ((53), (57), (58)) constrain the syntactic class of every word as long as the window. An idempotent class of a nonempty word is the class of arbitrarily long words, so it is constrained whatever the window ((56)–(58)), and an idempotent that fails the equation refutes the class for every window at once.

theorem Lambert2026.amara_not_isDefinite_one : ¬amara.IsDefinite 1

Stress-penult is not 1-definite (§2.1), since the class [σ] is not a right zero, with [σ] [σ] ≠ [σ] in the context σ́ __ (§6.2).

theorem Lambert2026.finnish_not_isDefinite (k : ℕ) : ¬finnish.IsDefinite k

Stress-initial is not definite (§2.2), since the class [σ] is idempotent but [σ́] [σ] ≠ [σ], with σ́σ in and σ out (§6.2.2).

theorem Lambert2026.amara_not_isReverseDefinite (k : ℕ) : ¬amara.IsReverseDefinite k

Stress-penult is not reverse definite (§6.2.2), since the class [σσ] is idempotent, as stress-penult is 2-definite, but [σσ] [σ́] ≠ [σσ] in the context __ σ.

theorem Lambert2026.stressPenultCulminative_not_isGeneralizedDefinite (k : ℕ) : ¬stressPenultCulminative.IsGeneralizedDefinite k

Culminative stress-penult is not generalized definite (§6.3), since the class [σσ] is idempotent but [σσ] [σ́] [σσ] ≠ [σσ] in the context __ σ́σ.

theorem Lambert2026.stressPenultCulminative_not_isBTK (k : ℕ) : ¬Language.IsBTK k stressPenultCulminative

Culminative stress-penult is not multitier reverse definite (§6.3), since in its syntactic monoid [σσ] is idempotent but [σσ] [σ́] [σσ] ≠ [σσ] [σ́] in the context __ σ, against the equation of (62).