Sandwich words: replicate kL aL ++ mid ++ replicate kR aR

A sandwich word is a list of the form replicate kL aL ++ mid ++ replicate kR aR — kL copies of the left bookend aL, then a middle, then kR copies of the right bookend aR. Bookends may be asymmetric (aL ≠ aR, kL ≠ kR), accommodating both symmetric phenomena (e.g. @cite{lambert-2026} §5.1 Luganda, where aL = aR = low) and asymmetric ones (e.g. @cite{lambert-2026} §4.2 Tsuut'ina, where aL = posterior, aR = anterior).

This shape is the workhorse of @cite{lambert-2026}'s parameterised counterexamples to multitier generalised definiteness (IsBTLI k): given a phonotactic constraint, exhibit two sandwich words sharing the same bookends that differ in the target language but match on every length-k tier-affix. The substrate factors out the algebraic content:

• takeAt_left_sandwich / takeAt_right_sandwich — tier-affixes always project to replicate k aL / replicate k aR regardless of mid, provided k ≤ kL / k ≤ kR.
• filter_sandwich_* — filtering preserves the sandwich shape, with bookend widths becoming 0 when the bookend character is dropped.
• sublist_sandwich_of_sublist_mid — any sublist of mid is a sublist of the sandwich.
• not_sublist_sandwich — under non-bookend conditions on the pattern's head and last element, a sublist of the sandwich must come from mid alone.

The symmetric specialisation aL = aR, kL = kR is handled by passing the same arguments twice; no separate definition is provided.

def Core.Computability.Subregular.sandwich {α : Type u_1} (kL : ℕ) (aL : α) (mid : List α) (kR : ℕ) (aR : α) : List α

A sandwich word with possibly asymmetric bookends: kL copies of aL on the left, then mid, then kR copies of aR on the right.

Equations

• Core.Computability.Subregular.sandwich kL aL mid kR aR = List.replicate kL aL ++ mid ++ List.replicate kR aR

@[simp]

theorem Core.Computability.Subregular.length_sandwich {α : Type u_1} {kL : ℕ} {aL : α} {mid : List α} {kR : ℕ} {aR : α} : (sandwich kL aL mid kR aR).length = kL + mid.length + kR

theorem Core.Computability.Subregular.takeAt_left_sandwich {α : Type u_1} {k kL : ℕ} {aL : α} {mid : List α} {kR : ℕ} {aR : α} (h : k ≤ kL) : Edge.left.takeAt k (sandwich kL aL mid kR aR) = List.replicate k aL

The length-k left tier-affix of a sandwich is replicate k aL, provided the left bookend is at least k wide. Side condition keeps this from @[simp] tagging — callers rw explicitly.

theorem Core.Computability.Subregular.takeAt_right_sandwich {α : Type u_1} {k kL : ℕ} {aL : α} {mid : List α} {kR : ℕ} {aR : α} (h : k ≤ kR) : Edge.right.takeAt k (sandwich kL aL mid kR aR) = List.replicate k aR

The length-k right tier-affix of a sandwich is replicate k aR, provided the right bookend is at least k wide. Side condition keeps this from @[simp] tagging — callers rw explicitly.

theorem Core.Computability.Subregular.filter_sandwich_of_pos_pos {α : Type u_1} {T : α → Bool} {aL aR : α} (hL : T aL = true) (hR : T aR = true) {kL : ℕ} {mid : List α} {kR : ℕ} : List.filter T (sandwich kL aL mid kR aR) = sandwich kL aL (List.filter T mid) kR aR

Sandwich filter, both bookends kept: shape preserved with original widths.

theorem Core.Computability.Subregular.filter_sandwich_of_neg_pos {α : Type u_1} {T : α → Bool} {aL aR : α} (hL : ¬T aL = true) (hR : T aR = true) {kL : ℕ} {mid : List α} {kR : ℕ} : List.filter T (sandwich kL aL mid kR aR) = List.filter T mid ++ List.replicate kR aR

Sandwich filter, left bookend dropped, right kept.

theorem Core.Computability.Subregular.filter_sandwich_of_pos_neg {α : Type u_1} {T : α → Bool} {aL aR : α} (hL : T aL = true) (hR : ¬T aR = true) {kL : ℕ} {mid : List α} {kR : ℕ} : List.filter T (sandwich kL aL mid kR aR) = List.replicate kL aL ++ List.filter T mid

Sandwich filter, left bookend kept, right dropped.

theorem Core.Computability.Subregular.filter_sandwich_of_neg_neg {α : Type u_1} {T : α → Bool} {aL aR : α} (hL : ¬T aL = true) (hR : ¬T aR = true) {kL : ℕ} {mid : List α} {kR : ℕ} : List.filter T (sandwich kL aL mid kR aR) = List.filter T mid

Sandwich filter, both bookends dropped: collapses to filtered middle.

theorem Core.Computability.Subregular.sublist_sandwich_of_sublist_mid {α : Type u_1} {pat mid : List α} (h : pat.Sublist mid) (kL : ℕ) (aL : α) (kR : ℕ) (aR : α) : pat.Sublist (sandwich kL aL mid kR aR)

Any sublist of the middle is a sublist of the sandwich.

theorem Core.Computability.Subregular.not_sublist_sandwich {α : Type u_1} {pat mid : List α} {aL aR : α} (h_first : pat.head? ≠ some aL) (h_last : pat.getLast? ≠ some aR) (h_inner : ¬pat.Sublist mid) (kL kR : ℕ) : ¬pat.Sublist (sandwich kL aL mid kR aR)

A pattern that doesn't start with aL or end with aR, and isn't a sublist of mid, is not a sublist of the sandwich. The bookend replicate blocks can't supply the head or last element of pat, so any sublist witness must come from mid alone.