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

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

Main results

• Subregular.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 Subregular.Augmented (α : Type u_2) : Type u_2

The boundary-augmented alphabet: original symbols (some a) plus the boundary marker none.

Equations

• Subregular.Augmented α = List (Option α)

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

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

Equations

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

@[simp]

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

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

Boundary-vacuous relations

structure Subregular.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 Subregular.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.