Block-Structured Witnesses for Pumping-Lemma Arguments

A BlockWitness symbols p is the string s₀ᵖ s₁ᵖ ⋯ sₙ₋₁ᵖ formed by concatenating one block of length p per symbol in symbols. Such witnesses are the standard test strings for non-context-freeness arguments via the CFL pumping lemma.

Three downstream consumers in Linglib.Core.Computability.NonContextFree share this substrate: anbncndn, anbnc, and ambncmdn.

API

Structure and counting:

• BlockWitness symbols p — the witness construction.
• length_eq, length_take — size arithmetic.
• split_at — clean decomposition at any block boundary.
• filter_count — counts of in-alphabet symbols (each = p, by Nodup).
• mem_iff — membership characterization.

Position bridge and adjacency:

• getElem?_eq — the foundational position-to-symbol bridge: (BlockWitness symbols p)[i]? = symbols[i / p]?.
• not_both_in_vxy — the adjacency lemma: in any decomposition BlockWitness symbols p = u ++ vxy ++ z with |vxy| ≤ p, two symbols at block-index distance ≥ 2 cannot both appear in vxy. Used by every per-alphabet not_X_and_Y_in_vxy consumer in NonContextFree.lean as a one-line invocation with (by decide) discharging the Nodup and index-distance hypotheses.

def BlockWitness {α : Type u} (symbols : List α) (p : ℕ) : List α

A block-structured witness: concatenates one block of length p per symbol in symbols.

Equations

• BlockWitness symbols p = List.flatMap (fun (s : α) => List.replicate p s) symbols

@[simp]

theorem BlockWitness.nil {α : Type u} (p : ℕ) : BlockWitness [] p = []

@[simp]

theorem BlockWitness.cons {α : Type u} (s : α) (ss : List α) (p : ℕ) : BlockWitness (s :: ss) p = List.replicate p s ++ BlockWitness ss p

@[simp]

theorem BlockWitness.zero {α : Type u} (symbols : List α) : BlockWitness symbols 0 = []

theorem BlockWitness.length_eq {α : Type u} (symbols : List α) (p : ℕ) : (BlockWitness symbols p).length = symbols.length * p

theorem BlockWitness.split_at {α : Type u} (symbols : List α) (p i : ℕ) : BlockWitness symbols p = BlockWitness (List.take i symbols) p ++ BlockWitness (List.drop i symbols) p

The witness splits cleanly at any block boundary.

theorem BlockWitness.length_take {α : Type u} (symbols : List α) (p : ℕ) {i : ℕ} (hi : i ≤ symbols.length) : (BlockWitness (List.take i symbols) p).length = i * p

theorem BlockWitness.filter_count {α : Type u} [DecidableEq α] {symbols : List α} (hnd : symbols.Nodup) (p : ℕ) (s : α) : (List.filter (fun (x : α) => x == s) (BlockWitness symbols p)).length = if s ∈ symbols then p else 0

Filter count: each in-alphabet symbol contributes exactly p; absent symbols contribute 0. Requires symbols.Nodup so blocks don't merge.

theorem BlockWitness.mem_iff {α : Type u} [DecidableEq α] {symbols : List α} {p : ℕ} (hp : p ≥ 1) (s : α) : s ∈ BlockWitness symbols p ↔ s ∈ symbols

A symbol appears in BlockWitness symbols p iff it's in symbols (and p ≥ 1).

theorem BlockWitness.getElem?_eq {α : Type u} {symbols : List α} {p : ℕ} (hp : 0 < p) (i : ℕ) : (BlockWitness symbols p)[i]? = symbols[i / p]?

Position bridge. The character at position i in BlockWitness symbols p is symbols[i / p]: the symbol whose block contains position i. Stated with [?] (optional indexing) so the equation holds for all i — out-of-range positions yield none on both sides.

This is the foundational position-vs-symbol bridge that makes locality arguments trivial: any structural fact about which symbols can appear at which positions reduces to integer division on the block-length p.

theorem BlockWitness.not_both_in_vxy {α : Type u} [DecidableEq α] {symbols : List α} (hnd : symbols.Nodup) {p : ℕ} {s t : α} {i j : ℕ} (hi : symbols[i]? = some s) (hj : symbols[j]? = some t) (hij : j ≥ i + 2) {u vxy z : List α} (hw : BlockWitness symbols p = u ++ vxy ++ z) (hvxy : vxy.length ≤ p) : ¬(s ∈ vxy ∧ t ∈ vxy)

Adjacency lemma. Two symbols at block-index distance ≥ 2 cannot both appear in any vxy of length ≤ p arising from a decomposition BlockWitness symbols p = u ++ vxy ++ z.

Proof: each occurrence of s (resp. t) in vxy corresponds to a position in [|u|, |u| + |vxy|) whose block index (pos / p) equals i (resp. j) by Nodup. The two positions differ by less than |vxy| ≤ p, so their block indices differ by at most 1 — contradicting j ≥ i + 2.