Bridge: Autosegmental Tier ↔ TSL Tier Projection

The autosegmental tier formalism (Core.Tier, the Kleisli morphism α → Option β lifted via List.filterMap) and the subregular TSL formalism (Core.Computability.Subregular.tierProject) share a single underlying primitive: tierProject T is literally Core.Tier.apply (Core.Tier.byClass T), so the two reduce to one another by definition.

This file records the resulting rfl identity and provides a thin adapter for building a TSL_k grammar directly from a Bool-valued class predicate (the autosegmental constructor shape), so a phonological tier (tonal tier, sibilant tier, nasal tier) plugs into TSL machinery without restating projection or filtering.

What this enables

Phonological constraints already in the codebase (mkOCPOnTier in Theories/Phonology/OptimalityTheory/Constraints.lean, the tonal tier in Theories/Phonology/Tier.lean) reuse the same Tier.apply machinery as TSL grammars — the bridge is no longer a theorem to discharge but a definitional consequence.

theorem Phonology.Subregular.apply_byClass_eq_tierProject {α : Type u_1} (T : α → Prop) [DecidablePred T] (xs : List α) : (Core.Tier.byClass T).apply xs = Core.Computability.Subregular.tierProject T xs

Bridge identity (definitional): tierProject T is by definition Tier.apply (Tier.byClass T). After the 0.230.x consolidation onto Core.Tier and the subsequent Tier.byClass migration to Prop+Decidable, this is rfl.

def Phonology.Subregular.TSLGrammar.ofByClass {α : Type u_1} (k : ℕ) (p : α → Bool) (permitted : Set (Core.Computability.Subregular.Augmented α)) : Core.Computability.Subregular.TSLGrammar k α

Adapter: build a TSL_k grammar from a class-membership autosegmental tier given as a Bool predicate. The TSL tier predicate is (p · = true), giving the TSL projection that matches Tier.apply (Tier.byClass p) on every input. Provided as a convenience for callers whose class predicates arise from FeatureSpec-style Bool lookups; native Prop-valued predicates can construct TSLGrammar records directly.

Equations

• Phonology.Subregular.TSLGrammar.ofByClass k p permitted = { tier := fun (x : α) => p x = true, decTier := fun (a : α) => instDecidableEqBool (p a) true, permitted := permitted }

@[simp]

theorem Phonology.Subregular.tierProject_ofByClass {α : Type u_1} (k : ℕ) (p : α → Bool) (xs : List α) : Core.Computability.Subregular.tierProject (TSLGrammar.ofByClass k p ∅).tier xs = List.filter p xs

The TSL grammar built from byClass projects via the same filter as Tier.apply (Tier.byClass p).