Multitier Extensions of Subregular Classes

Generic Boolean closure of tier-projected language families @cite{lambert-2022} @cite{lambert-2026}. The construction proceeds in two stages:

1. Tier-projected family IsTierBased 𝒞 L: L is the preimage under some Boolean tier predicate of a language in 𝒞.
2. Boolean closure BoolClosure 𝒞 L: L is built from members of 𝒞 via finite intersection, union, and complement.

Composing the two: IsBTC 𝒞 := BoolClosure (IsTierBased 𝒞) is the multitier (Boolean tier-projected) closure of 𝒞. Specializing yields the six classes Lambert (2026) tabulates:

• IsBTSL — multitier strictly local
• IsBTSP — multitier strictly piecewise
• IsBTD — multitier definite (e.g. Uyghur backness harmony per @cite{lambert-2026} §4.3, refining @cite{mayer-major-2018})
• IsBTK — multitier reverse definite
• IsBTLI — multitier generalized definite (e.g. Karanga Shona tone per @cite{lambert-2026} §5.6, refining @cite{jardine-2020})
• IsBTN — multitier finite-or-cofinite (e.g. culminativity)

Architecture

A single generic BoolClosure : (Language α → Prop) → Language α → Prop operator pays for itself across the six specializations and across other "closure-of-X" patterns elsewhere in linglib (IsLocallyTestable is arguably another instance, though kept structurally distinct for now). The mathlib analogue is Probability.Kernel.Defs general + Probability.Kernel.Deterministic specialized — generic operator at the top, one-line abbreviations downstream.

Tier representation: Bool, not Prop+DecidablePred

IsTierBased quantifies over tier predicates T : α → Bool. The Bool choice avoids the awkward ∃ T, ∃ _ : DecidablePred T, … quantifier shape and gives a decidable filter operation by construction. The existing tierProject (taking T : α → Prop with [DecidablePred T]) is recoverable via tierProject T = (·.filter (decide ∘ T)); the bridge to TSLGrammar lives in Tier.lean.

Decidability

IsBTC 𝒞 is a Prop-valued classifier; deciding membership of a specific language requires a finite witness (an automaton, a syntactic monoid). The decidability story lives in a separate DFA.isBTC style classifier, deferred to PR-3+.

Boolean closure of a language class

inductive Core.Computability.Subregular.BoolClosure {α : Type u_1} (𝒞 : Language α → Prop) : Language α → Prop

The Boolean closure of a class of languages 𝒞: the smallest predicate containing 𝒞 and closed under finite intersection, union, and complement. Free of base-class assumptions; the closure is empty iff 𝒞 is empty.

Constructors are the closure operations themselves; derived stability lemmas (top, bot, sdiff, finite intersections, …) live below or follow mechanically from the four primitives.

• base {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} : 𝒞 L → BoolClosure 𝒞 L

  Languages in the base class are in the closure.

• inter {α : Type u_1} {𝒞 : Language α → Prop} {L₁ L₂ : Language α} : BoolClosure 𝒞 L₁ → BoolClosure 𝒞 L₂ → BoolClosure 𝒞 (L₁ ⊓ L₂)

  Pairwise intersection (lattice ⊓, equiv. Set.inter via the CompleteAtomicBooleanAlgebra instance derived in mathlib's Language).

• union {α : Type u_1} {𝒞 : Language α → Prop} {L₁ L₂ : Language α} : BoolClosure 𝒞 L₁ → BoolClosure 𝒞 L₂ → BoolClosure 𝒞 (L₁ ⊔ L₂)

  Pairwise union (lattice ⊔; mathlib's Language derives the Boolean algebra, so ⊔ is union and + is the same operation under the Kleene algebra alias).

• compl {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} : BoolClosure 𝒞 L → BoolClosure 𝒞 Lᶜ

  Complement (Boolean algebra ᶜ).

theorem Core.Computability.Subregular.BoolClosure.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) {L : Language α} : BoolClosure 𝒞 L → BoolClosure 𝒟 L

The Boolean closure is monotone in the base class: enlarging 𝒞 enlarges the closure.

Tier-based language families

def Core.Computability.Subregular.IsTierBased {α : Type u_1} (𝒞 : Language α → Prop) (L : Language α) : Prop

A language L is tier-based for class 𝒞 iff there is some Boolean tier predicate T : α → Bool and some L' : Language α with L' in 𝒞 such that L is the preimage of L' under projection by T: w ∈ L ↔ w.filter T ∈ L'.

The Bool tier shape is the existence-friendly form (no instance quantifier issues). For the Prop+DecidablePred form used by tierProject and TSLGrammar, convert via T x ↔ tier x = true (see Tier.lean's TSLGrammar.ofByClass adapter).

Equations

• Core.Computability.Subregular.IsTierBased 𝒞 L = ∃ (T : α → Bool) (L' : Language α), L = {w : List α | List.filter T w ∈ L'} ∧ 𝒞 L'

theorem Core.Computability.Subregular.IsTierBased.of_class {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : 𝒞 L) : IsTierBased 𝒞 L

Class injection: every 𝒞-language is tier-based for 𝒞 via the universal-true tier (no symbols erased). The witness is T = fun _ => true and L' = L.

theorem Core.Computability.Subregular.IsTierBased.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) {L : Language α} (hL : IsTierBased 𝒞 L) : IsTierBased 𝒟 L

Monotonicity in the base class.

Multitier (Boolean tier-projected) closure

def Core.Computability.Subregular.IsBTC {α : Type u_1} (𝒞 : Language α → Prop) : Language α → Prop

The multitier closure of a class 𝒞: the Boolean closure of the tier-projected family. Lambert's B(TC) notation.

Equations

• Core.Computability.Subregular.IsBTC 𝒞 = Core.Computability.Subregular.BoolClosure (Core.Computability.Subregular.IsTierBased 𝒞)

theorem Core.Computability.Subregular.IsBTC.of_class {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : 𝒞 L) : IsBTC 𝒞 L

Class injection into the multitier closure: every 𝒞-language is in IsBTC 𝒞. Composed of IsTierBased.of_class (universal tier) and BoolClosure.base.

theorem Core.Computability.Subregular.IsBTC.of_tierBased {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : IsTierBased 𝒞 L) : IsBTC 𝒞 L

Tier-based injection into the multitier closure: every tier-based-for-𝒞 language is in IsBTC 𝒞.

theorem Core.Computability.Subregular.IsBTC.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) {L : Language α} : IsBTC 𝒞 L → IsBTC 𝒟 L

Monotonicity of multitier closure in the base class.

Specializations: Lambert (2026) Table 6

One line each. Closure under intersection, union, and complement comes from BoolClosure's constructors; class injection from IsBTC.of_class.

def Core.Computability.Subregular.IsBTSL {α : Type u_1} (k : ℕ) : Language α → Prop

Multitier strictly local (BTSL): Boolean closure of tier-projected SL_k languages.

Equations

• Core.Computability.Subregular.IsBTSL k = Core.Computability.Subregular.IsBTC (Core.Computability.Subregular.IsStrictlyLocal k)

def Core.Computability.Subregular.IsBTSP {α : Type u_1} (k : ℕ) : Language α → Prop

Multitier strictly piecewise (BTSP): Boolean closure of tier-projected SP_k languages.

Equations

• Core.Computability.Subregular.IsBTSP k = Core.Computability.Subregular.IsBTC (Core.Computability.Subregular.IsStrictlyPiecewise k)

def Core.Computability.Subregular.IsBTD {α : Type u_1} (k : ℕ) : Language α → Prop

Multitier definite (BTD): Boolean closure of tier-projected D_k languages. Lambert (2026) §4.3 places Uyghur backness harmony in this class — strictly stronger than the multiple-tier-based strictly-local class of @cite{de-santo-graf-2019}.

Equations

• Core.Computability.Subregular.IsBTD k = Core.Computability.Subregular.IsBTC (Core.Computability.Subregular.IsDefinite k)

def Core.Computability.Subregular.IsBTK {α : Type u_1} (k : ℕ) : Language α → Prop

Multitier reverse definite (BTK): Boolean closure of tier-projected RD_k languages.

Equations

• Core.Computability.Subregular.IsBTK k = Core.Computability.Subregular.IsBTC (Core.Computability.Subregular.IsReverseDefinite k)

def Core.Computability.Subregular.IsBTLI {α : Type u_1} (k : ℕ) : Language α → Prop

Multitier generalized definite (BTLI): Boolean closure of tier-projected ℒℐ_k languages. Lambert (2026) §5.6 places Karanga Shona tone in this class (verb-stem domain) — refining @cite{jardine-2020}.

Equations

• Core.Computability.Subregular.IsBTLI k = Core.Computability.Subregular.IsBTC (Core.Computability.Subregular.IsGeneralizedDefinite k)

def Core.Computability.Subregular.IsBTN {α : Type u_1} : Language α → Prop

Multitier finite-or-cofinite (BTN): Boolean closure of tier-projected co/finite languages. Captures culminativity-style constraints when projected to the stress tier.

Equations

• Core.Computability.Subregular.IsBTN = Core.Computability.Subregular.IsBTC Core.Computability.Subregular.IsFiniteOrCofinite

Cross-class inclusions

Class containment lifts through the multitier construction: if 𝒞 ⊆ 𝒟 pointwise, then IsBTC 𝒞 ⊆ IsBTC 𝒟. Specializing yields the standard inclusions BTSL ⊆ BTSP, BTD ⊆ BTLI, BTK ⊆ BTLI, BTN ⊆ BTLI (per Lambert (2026) Table 6 and the §2.4 small hierarchy diagram).

theorem Core.Computability.Subregular.IsBTD.toIsBTLI {α : Type u_1} {k : ℕ} {L : Language α} (h : IsBTD k L) : IsBTLI k L

D_k ⊆ ℒℐ_k lifts to BTD_k ⊆ BTLI_k.

theorem Core.Computability.Subregular.IsBTK.toIsBTLI {α : Type u_1} {k : ℕ} {L : Language α} (h : IsBTK k L) : IsBTLI k L

RD_k ⊆ ℒℐ_k lifts to BTK_k ⊆ BTLI_k.

Bridge: TSL ↔ tier-based SL

theorem Core.Computability.Subregular.isTierStrictlyLocal_iff_isTierBased_isStrictlyLocal {α : Type u_1} {k : ℕ} {L : Language α} : IsTierStrictlyLocal k L ↔ IsTierBased (IsStrictlyLocal k) L

TSL_k = IsTierBased (IsStrictlyLocal k). The TSLGrammar-witnessed predicate IsTierStrictlyLocal and the generic preimage-of-SL predicate IsTierBased ∘ IsStrictlyLocal are co-extensive on Language α. The bridge gives every existing IsTierStrictlyLocal witness a free IsBTSL corollary via BoolClosure.base.

theorem Core.Computability.Subregular.IsTierStrictlyLocal.toIsBTSL {α : Type u_1} {k : ℕ} {L : Language α} (h : IsTierStrictlyLocal k L) : IsBTSL k L

TSL_k → BTSL_k: every tier-based strictly local language is in the multitier closure of strictly local languages. Combines the bridge with BoolClosure.base.

Indistinguishability framework for refuting IsBTC membership

Standard mathematical technique for L ∉ IsBTC 𝒞: exhibit two words w₁, w₂ that are 𝒞-tier-indistinguishable (every 𝒞-language under every Bool tier projection assigns them the same membership) but differ in L-membership. Lambert (2026) §4.2 (Tsuut'ina) and §5.1 (Luganda) both use this technique with the specialization for IsGeneralizedDefinite k (sharing length-k prefix-and-suffix on every tier projection — see indist_isGenDef_of_tierAffixes).

def Core.Computability.Subregular.IsBTC.Indist {α : Type u_1} (𝒞 : Language α → Prop) (w₁ w₂ : List α) : Prop

Two words are 𝒞-tier-indistinguishable iff under every Bool tier projection, every 𝒞-language assigns them the same membership.

Equations

• Core.Computability.Subregular.IsBTC.Indist 𝒞 w₁ w₂ = ∀ (T : α → Bool) (L' : Language α), 𝒞 L' → (List.filter T w₁ ∈ L' ↔ List.filter T w₂ ∈ L')

theorem Core.Computability.Subregular.IsBTC.Indist.refl {α : Type u_1} (𝒞 : Language α → Prop) (w : List α) : Indist 𝒞 w w

theorem Core.Computability.Subregular.IsBTC.Indist.symm {α : Type u_1} {𝒞 : Language α → Prop} {w₁ w₂ : List α} (h : Indist 𝒞 w₁ w₂) : Indist 𝒞 w₂ w₁

theorem Core.Computability.Subregular.IsBTC.mem_iff_of_indist {α : Type u_1} {𝒞 : Language α → Prop} {w₁ w₂ : List α} {L : Language α} (hL : IsBTC 𝒞 L) (hindist : Indist 𝒞 w₁ w₂) : w₁ ∈ L ↔ w₂ ∈ L

Tier-indistinguishability transports through the Boolean closure: w₁ and w₂ 𝒞-tier-indistinguishable implies same membership in every IsBTC 𝒞-language. Proof by induction on BoolClosure: base is the defining property of Indist; inter/union/compl lift via and_congr/or_congr/not_congr.

theorem Core.Computability.Subregular.not_isBTC_of_indist {α : Type u_1} {𝒞 : Language α → Prop} {w₁ w₂ : List α} {L : Language α} (h_indist : IsBTC.Indist 𝒞 w₁ w₂) (h_w₁ : w₁ ∈ L) (h_w₂ : w₂ ∉ L) : ¬IsBTC 𝒞 L

Refutation lemma: if w₁ ∈ L and w₂ ∉ L but w₁ and w₂ are 𝒞-tier-indistinguishable, then L ∉ IsBTC 𝒞.

theorem Core.Computability.Subregular.IsBTC.indist_isGenDef_of_tierAffixes {α : Type u_1} {k : ℕ} {w₁ w₂ : List α} (h : ∀ (T : α → Bool), Edge.left.takeAt k (List.filter T w₁) = Edge.left.takeAt k (List.filter T w₂) ∧ Edge.right.takeAt k (List.filter T w₁) = Edge.right.takeAt k (List.filter T w₂)) : Indist (IsGeneralizedDefinite k) w₁ w₂

Shared length-k prefix-and-suffix on every Bool-tier projection implies IsBTC.Indist (IsGeneralizedDefinite k). This is the standard specialization Lambert (2026) §4.2 / §5.1 use for refuting IsBTLI k membership: producing two words with matching tier-affixes on every tier reduces to providing a Bool-tier-parameterised pair of equalities.