CFL pumping lemma — machine-checked from scratch in Lean (cfl_pumping) (#106)

## Summary

Machine-checks the **pumping lemma for context-free languages** — a
result even Mathlib lacks — built from scratch in core Lean
(Mathlib-free, single-file, `lean
docs/proofs/verification/WokeGrammarPumping.lean`).

`cfl_pumping`: for an ε-free binary-normal-form grammar with `card`
nonterminals, any word `z ∈ L(S)` of length `≥ 2^(card+1)` decomposes as
`z = u v w x y` with
- `1 ≤ |v x|` (the pumped part is non-empty — uses ε-freeness),
- `|v w x| ≤ 2^(card+1)` (the window is bounded),
- `u vⁱ w xⁱ y ∈ L(S)` for every `i`.

## What's in the file (`WokeGrammarPumping.lean`)

Foundation (landed first):
- parse trees `PT` over a binary-normal-form grammar; `yield_bound`
(`|w| < 2^height`);
- one-hole contexts `Ctx` + `fill`; `pumpIter` (the pumping operation);
- `spine`/`spine_length`; a Mathlib-free finite `pigeon`hole.

Assembly (this completes it):
- `Ctx.comp` — context composition;
- `descend` — tallest-spine descent (recursion on **depth** so it
reduces definitionally);
- `ht_descend` — descended-subtree height is `ht t − d`;
- `nodeNT_add` — depth-composition law that locates the repeated
nonterminal;
- `yield_nonempty` / `descend_sibling_nonempty` — ε-free ⇒ `|v x| ≥ 1`;
- `cfl_pumping` — pigeonhole over the bottom `card+1` spine nodes ⇒
outer·pump·base ⇒ pump via `pumpIter`.

## Trust base

The three standard classical kernel constants (`propext`,
`Classical.choice`, `Quot.sound`) — the same foundations Mathlib relies
on (`Classical.choice` enters via the `pigeon` case split). No holes and
no project-specific assumptions; every step is checked by Lean's kernel.

## Verification

`lean docs/proofs/verification/WokeGrammarPumping.lean` exits 0 with no
errors (wired into `.github/workflows/lean-proofs.yml`).

Docs updated: `grammar-proofs.md` §7.3 and `GRAMMAR-PROOF-INVENTORY.md`
record the pumping lemma as machine-checked. The §7.3 ∩/¬ non-closure
corollary (finite `IsCFL` + `aⁿbⁿcⁿ ∉ CFL` + De Morgan) is the remaining
increment, now unblocked.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/lean-proofs.yml

@@ -68,3 +68,9 @@ jobs:
           set -euo pipefail
           lean docs/proofs/verification/WokeGrammarCFL.lean
           echo "✅ WokeGrammarCFL.lean verified"
+
+      - name: Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation)
+        run: |
+          set -euo pipefail
+          lean docs/proofs/verification/WokeGrammarPumping.lean
+          echo "✅ WokeGrammarPumping.lean verified"

docs/proofs/formal-semantics/grammar-proofs.md

@@ -328,8 +328,12 @@ The binding power comparison ensures this:
 > §7.3 **CFL closure under ∪, ·, \*** is now machine-checked too, in
 > [`../verification/WokeGrammarCFL.lean`](../verification/WokeGrammarCFL.lean)
 > (a CFG derivation relation + union/concat/star grammar constructions,
-> Mathlib-free, `sorry`-free). Only the §7.3 *non*-closure under ∩ / ¬ remains
-> scoped (it needs the pumping lemma for CFLs); status in
+> Mathlib-free, `sorry`-free). The **pumping lemma for context-free languages**
+> — which even Mathlib lacks — is now machine-checked from scratch in core Lean in
+> [`../verification/WokeGrammarPumping.lean`](../verification/WokeGrammarPumping.lean)
+> (`cfl_pumping`: parse-tree spine navigation + finite pigeonhole ⇒ the `uvwxy`
+> decomposition with `1 ≤ |vx|` and `|vwx| ≤ 2^(card+1)`). Only the §7.3 *non*-closure
+> under ∩ / ¬ remains, and the pumping lemma it needed is now available; status in
 > `../verification/GRAMMAR-PROOF-INVENTORY.md`.
 
 ### 7.1 Chomsky Hierarchy Position

docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md

@@ -71,7 +71,8 @@ reach here, with reason).
 | T1.2 | §1.1 LL(1) = ✗ | ✅ | **P4** | Exhibit the FIRST/FIRST conflict (`primary → identifier` vs `identifier "(" …`) — a 1-lookahead non-determinism witness | MACHINE-CHECKED |
 | T7.3a | §7.3 CFL closed under ∪, ·, * | ✅ done from scratch | **P5→done** | `WokeGrammarCFL.lean`: CFG derivation relation + reusable embedding lemma + union/concat/star grammar constructions, `propext`-only | MACHINE-CHECKED |
 | T7.1 | §7.1 Not regular (pumping lemma) | ✅ done from scratch | **P6→done** | `WokeGrammarRegular.lean`: bespoke finite pigeonhole + `Fin k` DFA + fooling-set on `aⁿbⁿ` (≅ `(ⁿ)ⁿ`), Mathlib-free | MACHINE-CHECKED |
-| T7.3b | §7.3 CFL **not** closed under ∩, ¬ | ⚠️ no (needs non-CFL-ness of `aⁿbⁿcⁿ`) | **P6** | Requires the pumping lemma *for CFLs* — same Mathlib gap | FLAGGED |
+| T7.0 | CFL pumping lemma (Mathlib-gap) | ✅ done from scratch | **Ext** | `WokeGrammarPumping.lean`: `cfl_pumping` — `descend`/`ht_descend`/`nodeNT_add` spine navigation + `Ctx.comp` + pigeonhole ⇒ `z = uvwxy`, `1≤|vx|`, `|vwx|≤2^(card+1)`, `uvⁱwxⁱy ∈ L`; classical kernel constants only | MACHINE-CHECKED |
+| T7.3b | §7.3 CFL **not** closed under ∩, ¬ | ⚠️ remaining (pumping lemma now available) | **P6** | The blocker (CFL pumping lemma) is now proved as T7.0; remaining: finite `IsCFL` + `aⁿbⁿcⁿ ∉ CFL` + De Morgan | IN PROGRESS |
 
 ## Priority order (execution)
 
@@ -162,7 +163,7 @@ universal `prefix_rt`/`completeness_rp` development; a Coq port of that is the
 scoped next step, exactly as `WokeLang.{lean,v}` are "complementary, not
 identical" per `AUDIT.md`.)
 
-## §7 — status (T7.1 done from scratch; §7.3 scoped)
+## §7 — status (T7.1 done; §7.3 positive closure + CFL pumping lemma done)
 
 - **T7.1 not regular — DONE** (`WokeGrammarRegular.lean`): rather than fetch
   Mathlib's automata library (blocked offline), a bespoke finite pigeonhole + a
@@ -174,9 +175,22 @@ identical" per `AUDIT.md`.)
   (`embGen_iff`) + explicit union/concat/star grammar constructions, `sorry`-free
   (`propext`-only). The WokeLang surface grammar is context-free, so it inhabits
   this class and these operations apply.
-- **§7.3 *non-closure* under ∩ / ¬** is still scoped: it needs the pumping lemma
-  **for CFLs** (e.g. to show `aⁿbⁿcⁿ` is not context-free), a separate larger
-  development — recorded rather than stubbed.
+- **Pumping lemma for CFLs — DONE** (`WokeGrammarPumping.lean`): the full pumping
+  lemma (which even Mathlib lacks) is now machine-checked from scratch in core
+  Lean. `cfl_pumping` states that for an ε-free binary-normal-form grammar with
+  `card` nonterminals, any word `z ∈ L(S)` of length `≥ 2^(card+1)` splits as
+  `z = u v w x y` with `1 ≤ |v x|`, `|v w x| ≤ 2^(card+1)`, and `u vⁱ w xⁱ y ∈
+  L(S)` for all `i`. Engine: parse trees + `|w| < 2^height` yield bound + one-hole
+  contexts/`fill`/`comp` + `pumpIter` + tallest-spine `descend` (with the
+  `ht = height − depth` and depth-composition laws) + finite pigeonhole ⇒
+  repeated-nonterminal extraction. Trust base: the three classical kernel
+  constants (`propext`, `Classical.choice`, `Quot.sound`) — no holes, no
+  project-specific assumptions.
+- **§7.3 *non-closure* under ∩ / ¬** is the remaining increment. With the pumping
+  lemma in hand it follows by the standard route: a finiteness-aware `IsCFL` (the
+  relation-based `IsCFL` is too permissive here — an infinite nonterminal type
+  could "generate" `aⁿbⁿcⁿ`), then `aⁿbⁿcⁿ ∉ CFL` via `cfl_pumping`, then
+  `L₁ ∩ L₂` non-closure by De Morgan against the proven positive ∪ closure.
 
 ## Status