Multitier extensions of subregular classes

The Boolean closure of tier-projected language families. For a class 𝒞 : Language α → Prop, the multitier closure IsBTC 𝒞 closes under finite ⊓/⊔/ᶜ the languages that are preimages of a 𝒞-language under some Boolean tier projection.

Main definitions

• IsTierBased 𝒞 — preimages of 𝒞-languages under a Boolean tier projection.
• IsBTC 𝒞 — the multitier closure: the BooleanSubalgebra.closure of the tier-projected family, with injections IsBTC.base/of_class and closure operations IsBTC.inter/union/compl.
• IsBTSL/IsBTSP/IsBTD/IsBTK/IsBTLI/IsBTN — its six specializations (strictly local, strictly piecewise, definite, reverse definite, generalized definite, finite-or-cofinite).
• IsBTC.Indist — tier-indistinguishability, the congruence behind membership refutation.

Main results

• IsBTC.mono — monotonicity in the base class.
• IsBTC.mem_iff_of_indist and not_isBTC_of_indist — membership respects tier-indistinguishability, yielding the standard non-membership argument.

Implementation notes

IsTierBased/IsBTC.Indist quantify over Bool tiers T : α → Bool, avoiding an ∃ T, ∃ _ : DecidablePred T, … witness; the Prop-with-[DecidablePred] form used by tierProject/TSLGrammar converts via T x ↔ tier x = true.

Tier-based language families

def Language.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.

Equations

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

theorem Language.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 Language.IsTierBased.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} {L : Language α} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) (hL : IsTierBased 𝒞 L) : IsTierBased 𝒟 L

Monotonicity in the base class.

Multitier (Boolean tier-projected) closure

def Language.IsBTC {α : Type u_1} (𝒞 : Language α → Prop) (L : Language α) : Prop

The multitier closure of a class 𝒞: the Boolean subalgebra of Language α generated by the tier-projected family IsTierBased 𝒞.

Equations

• Language.IsBTC 𝒞 L = (L ∈ BooleanSubalgebra.closure {L' : Language α | Language.IsTierBased 𝒞 L'})

theorem Language.IsBTC.base {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : IsTierBased 𝒞 L) : IsBTC 𝒞 L

Base-class injection: a tier-based language lies in the closure.

theorem Language.IsBTC.inter {α : Type u_1} {𝒞 : Language α → Prop} {L₁ L₂ : Language α} (h₁ : IsBTC 𝒞 L₁) (h₂ : IsBTC 𝒞 L₂) : IsBTC 𝒞 (L₁ ⊓ L₂)

Closure under intersection.

theorem Language.IsBTC.union {α : Type u_1} {𝒞 : Language α → Prop} {L₁ L₂ : Language α} (h₁ : IsBTC 𝒞 L₁) (h₂ : IsBTC 𝒞 L₂) : IsBTC 𝒞 (L₁ ⊔ L₂)

Closure under union.

theorem Language.IsBTC.compl {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : IsBTC 𝒞 L) : IsBTC 𝒞 Lᶜ

Closure under complement.

theorem Language.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 𝒞, via the universal tier.

theorem Language.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 Language.IsBTC.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} {L : Language α} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) (hL : IsBTC 𝒞 L) : IsBTC 𝒟 L

Monotonicity of multitier closure in the base class.

Specializations

One line each. Closure under intersection, union, and complement comes from IsBTC.inter/union/compl; class injection from IsBTC.of_class.

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

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

Equations

• Language.IsBTSL k = Language.IsBTC fun (x : Language α) => x.IsStrictlyLocal k

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

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

Equations

• Language.IsBTSP k = Language.IsBTC fun (x : Language α) => x.IsStrictlyPiecewise k

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

Multitier definite (BTD): Boolean closure of tier-projected D_k languages.

Equations

• Language.IsBTD k = Language.IsBTC fun (x : Language α) => x.IsDefinite k

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

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

Equations

• Language.IsBTK k = Language.IsBTC fun (x : Language α) => x.IsReverseDefinite k

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

Multitier generalized definite (BTLI): Boolean closure of tier-projected ℒℐ_k languages.

Equations

• Language.IsBTLI k = Language.IsBTC fun (x : Language α) => x.IsGeneralizedDefinite k

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

Multitier finite-or-cofinite (BTN): Boolean closure of tier-projected co/finite languages.

Equations

• Language.IsBTN = Language.IsBTC Language.IsFiniteOrCofinite

Cross-class inclusions

Class containment lifts through the multitier construction: if 𝒞 ⊆ 𝒟 pointwise, then IsBTC 𝒞 ⊆ IsBTC 𝒟. Specializing the D_k ⊆ ℒℐ_k and RD_k ⊆ ℒℐ_k inclusions yields BTD ⊆ BTLI and BTK ⊆ BTLI.

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

D_k ⊆ ℒℐ_k lifts to BTD_k ⊆ BTLI_k.

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

RD_k ⊆ ℒℐ_k lifts to BTK_k ⊆ BTLI_k.

TSL ⊆ multitier SL

theorem Language.IsTierStrictlyLocal.toIsBTSL {α : Type u_1} {L : Language α} {k : ℕ} (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. A TSLGrammar witness presents its language as the preimage of an SL language under the tier projection, hence IsTierBased (Language.IsStrictlyLocal · k), hence in the closure via IsBTC.base.

Indistinguishability framework for refuting IsBTC membership

Standard 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. The IsGeneralizedDefinite k specialization — sharing length-k prefix-and-suffix on every tier projection (indist_isGenDef_of_tierAffixes) — is the common case.

def Language.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

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

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

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

theorem Language.IsBTC.Indist.trans {α : Type u_1} {𝒞 : Language α → Prop} {w₁ w₂ w₃ : List α} (h₁ : Indist 𝒞 w₁ w₂) (h₂ : Indist 𝒞 w₂ w₃) : Indist 𝒞 w₁ w₃

theorem Language.IsBTC.mem_iff_of_indist {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} {w₁ w₂ : List α} (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. Induction on the closure: mem is the defining property of Indist; bot/sup/compl lift via Iff.rfl/or_congr/not_congr.

theorem Language.not_isBTC_of_indist {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} {w₁ w₂ : List α} (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 Language.IsBTC.indist_isGenDef_of_tierAffixes {α : Type u_1} {k : ℕ} {w₁ w₂ : List α} (h : ∀ (T : α → Bool), Subregular.Edge.left.takeAt k (List.filter T w₁) = Subregular.Edge.left.takeAt k (List.filter T w₂) ∧ Subregular.Edge.right.takeAt k (List.filter T w₁) = Subregular.Edge.right.takeAt k (List.filter T w₂)) : Indist (fun (x : Language α) => x.IsGeneralizedDefinite k) w₁ w₂

Shared length-k prefix-and-suffix on every Bool-tier projection implies IsBTC.Indist (Language.IsGeneralizedDefinite · k) — the standard specialization for refuting IsBTLI k membership, reducing it to a Bool-tier-parameterised pair of affix equalities.