Subregular Languages: Boundary Augmentation

Boundary augmentation of strings and a boundary-vacuity predicate relating the chain-membership of a padded string to that of its unpadded core. The strictly-local, locally-testable, and tier-relativized classes are built on this infrastructure [Lam22a] [HR10] [RP11]. The contiguous k-factors the hierarchy quantifies over are a generic list combinator and live in Core/Data/List/Factors.lean (List.kFactors).

Main definitions

• Augmented α: boundary-augmented strings List (Option α), with none the boundary marker.
• boundary k w: w injected into Augmented α and padded with k - 1 boundary markers on each side.
• IsBoundaryVacuous R: R holds whenever either argument is the boundary marker none.

Main results

• IsBoundaryVacuous.isChain_boundary_two_iff: boundary padding does not change IsChain-membership for a boundary-vacuous relation.

Implementation notes

The standard subregular convention extends the alphabet with two edge markers ⋊, ⋉ and studies the k-factors of ⋊ᵏ⁻¹ · w · ⋉ᵏ⁻¹. We instead use the one-fresh-symbol extension Option α (none = boundary, some a = original symbol): a single marker suffices because boundary symbols only ever occur at fixed positions, so the two edges are never confused.

Boundary augmentation

@[reducible, inline]

abbrev Augmented (α : Type u_2) : Type u_2

Boundary-augmented strings: original symbols (some a) plus the boundary marker none.

Equations

• Augmented α = List (Option α)

def boundary {α : Type u_1} (k : ℕ) (w : List α) : Augmented α

w padded with k - 1 boundary markers (none) on each side.

Equations

• boundary k w = List.replicate (k - 1) none ++ List.map some w ++ List.replicate (k - 1) none

@[simp]

theorem boundary_one {α : Type u_1} (w : List α) : boundary 1 w = List.map some w

theorem length_boundary {α : Type u_1} (k : ℕ) (w : List α) : List.length (boundary k w) = w.length + 2 * (k - 1)

Position discrimination and the configuration bridge

Entries of boundary k y are values of the word's two-sided configuration (List.config), shifted by the pad width; consequently the k-factors of the augmented word are exactly its windows (List.window).

theorem getElem?_boundary {α : Type u_1} {k : ℕ} {w : List α} (j : ℕ) : (boundary k w)[j]? = if j < k - 1 then some none else if j < k - 1 + w.length then Option.map some w[j - (k - 1)]? else if j < w.length + 2 * (k - 1) then some none else none

The augmented string's entries by region: left pad, letters, right pad.

theorem of_getElem?_boundary_eq_some {α : Type u_1} {k : ℕ} {w : List α} {j : ℕ} {a : α} (h : (boundary k w)[j]? = some (some a)) : k - 1 ≤ j ∧ w[j - (k - 1)]? = some a

A letter entry sits in the letter region.

theorem of_getElem?_boundary_eq_none {α : Type u_1} {k : ℕ} {w : List α} {j : ℕ} (h : (boundary k w)[j]? = some none) : j < k - 1 ∨ k - 1 + w.length ≤ j

A marker entry sits in one of the pads.

theorem getElem?_boundary_eq_config {α : Type u_1} {k : ℕ} {w : List α} {q : ℕ} (h : q < w.length + 2 * (k - 1)) : (boundary k w)[q]? = some (w.config (↑q - ↑(k - 1)))

Boundary entries are configuration values, shifted by the pad width.

theorem mem_kFactors_boundary_iff {α : Type u_1} {k : ℕ} {y : List α} {f : List (Option α)} (hk : 1 ≤ k) : f ∈ List.kFactors k (boundary k y) ↔ ∃ (i : ℤ), 1 - ↑k ≤ i ∧ i < ↑y.length ∧ f = List.window k y i

The k-factors of the augmented word are exactly its windows over [1 - k, w.length).

Boundary-vacuous relations

structure IsBoundaryVacuous {α : Type u_1} (R : Option α → Option α → Prop) : Prop

A relation on Option α is boundary-vacuous when none satisfies it on either side (R none u, R u none) — so only (some a, some b) pairs can witness a violation. Subregular edge constraints (OCP, no-clash, no-lapse) all share this shape.

• none_left (u : Option α) : R none u
• none_right (u : Option α) : R u none

theorem IsBoundaryVacuous.isChain_boundary_two_iff {α : Type u_1} {R : Option α → Option α → Prop} (hR : IsBoundaryVacuous R) (ys : List α) : List.IsChain R (boundary 2 ys) ↔ List.IsChain R (List.map some ys)

2-boundary padding preserves IsChain for a boundary-vacuous relation.