hyperpolymath · hyperpolymath · Jun 27, 2026 · Jun 27, 2026 · Jun 27, 2026 · Jun 27, 2026
@@ -21,6 +21,6 @@ jobs:
         with:
           fetch-depth: 0
       - name: TruffleHog Secret Scan
-        uses: trufflesecurity/trufflehog@main
+        uses: trufflesecurity/trufflehog@30d5bb91af1a771378349dbbb0c82129392acf70 # v3.95.6
         with:
           extra_args: --only-verified --fail
@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 

@@ -0,0 +1,119 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# RESUME — grammar formal-proofs work
+
+Pick-up notes for continuing the `claude/v2-grammar-proofs-audit-1yqgxh` work on
+another machine (e.g. the Claude Code desktop app). Everything here is committed
+to that branch, so it travels with the code.
+
+## Where the work stands
+
+Goal: machine-check every necessary/sufficient proof for the grammar that exists
+in this repo (`grammar/wokelang.ebnf`), install the provers, and report only
+proofs that actually run. The grammar was reconciled to one source of truth, and
+the proof obligations were mechanized in Lean 4 (mirrored to Coq where sensible).
+
+**Open PR:** #106 — *CFL pumping lemma, machine-checked from scratch in Lean*
+(branch `claude/v2-grammar-proofs-audit-1yqgxh`).
+
+**Merged on the way here:** #102 (parser metatheory + grammar reconciliation),
+#103 (no-left-recursion + lexer + classification, Lean+Coq), #104 (Coq parser
+port + §7.1 not-regular), #105 (§7.3 CFL positive closure).
+
+## Proof inventory — all verified green (last full run in the cloud container)
+
+Single-file, Mathlib-free. `lean <file>` / `coqc <file>` must exit 0 with no errors.
+
+| File | What it proves | Status |
+|---|---|---|
+| `docs/proofs/verification/WokeLang.lean` / `.v` | core language metatheory (sorry-audit resolved) | ✅ |
+| `docs/proofs/verification/WokeGrammar.lean` | Pratt-parser metatheory: prefix/completeness/determinism/injectivity | ✅ |
+| `docs/proofs/verification/WokeGrammarStructure.lean` / `.v` | no-left-recursion (+ found a real spec bug in `pattern`), lexer maximal-munch + keyword priority, CFG/¬LL(1)/LL(2) classification | ✅ |
+| `docs/proofs/verification/WokeGrammarParser.v` | Coq port of the parser metatheory | ✅ |
+| `docs/proofs/verification/WokeGrammarRegular.lean` | §7.1 not-regular: bespoke pigeonhole + `Fin k` DFA + fooling set on `aⁿbⁿ` | ✅ |
+| `docs/proofs/verification/WokeGrammarCFL.lean` | §7.3 CFL **positive** closure under ∪, ·, * | ✅ |
+| `docs/proofs/verification/WokeGrammarPumping.lean` | **CFL pumping lemma** `cfl_pumping` (the Mathlib-gap result) | ✅ |
+
+Trust base for the proofs: the standard classical kernel constants only
+(`propext`, `Classical.choice`, `Quot.sound`) — no holes, no project-specific
+assumptions. Confirm with Lean's kernel-dependency printout per file.
+
+The claim-by-claim map lives in
+`docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md`.
+
+## How to re-run the provers locally
+
+The provers are NOT in the repo — they were installed in the (ephemeral) cloud
+container. Reinstall the pinned versions locally.
+
+### Lean 4.30.0 (pinned by `docs/proofs/verification/lean-toolchain`)
+
+The exact, Mathlib-free steps are in `.github/workflows/lean-proofs.yml`:
+
+```sh
+ver=4.30.0
+curl -sSL -o /tmp/lean.tar.zst \
+  "https://github.com/leanprover/lean4/releases/download/v${ver}/lean-${ver}-linux.tar.zst"
+sudo mkdir -p /opt/lean
+sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt/lean
+export PATH="/opt/lean/lean-${ver}-linux/bin:$PATH"   # use the macOS/win tarball on those OSes
+```
+
+Then, from the repo root:
+
+```sh
+for f in WokeLang WokeGrammar WokeGrammarStructure WokeGrammarRegular WokeGrammarCFL WokeGrammarPumping; do
+  lean docs/proofs/verification/$f.lean && echo "OK $f"
+done
+```
+
+### Coq 8.18.0
+
+```sh
+# install coq 8.18.0 (opam: `opam pin add coq 8.18.0`, or your platform package)
+cd docs/proofs/verification
+for f in WokeLang WokeGrammarStructure WokeGrammarParser; do coqc $f.v && echo "OK $f"; done
+rm -f *.vo *.vok *.vos *.glob .*.aux   # clean build artifacts
+```
+
+## §7.3 non-closure — status
+
+Done (in `WokeGrammarPumping.lean`):
+
+1. **Finiteness-aware `IsCFL`** — a language is CF iff some ε-free BNF grammar with
+   an `enum`/`card` nonterminal bound generates exactly it (matches `cfl_pumping`).
+2. **`aⁿbⁿcⁿ ∉ CFL`** (`anbncn_not_cfl`) — via `cfl_pumping`: pumping down to
+   `i = 0` forces `count_a = count_b = count_c` in the deleted part, so the window
+   spans an `a` and a `c`; the positional core (`prefix_pure`, `abc_window`) then
+   gives `|vwx| > p`, contradicting `|vwx| ≤ p`. This is the canonical non-CFL and
+   the crux of the ∩/¬ non-closure result.
+
+Remaining (next increment):
+
+3. **The explicit ∩ / ¬ non-closure statement** — exhibit the two witness CFLs
+   `L₁ = {aⁿbⁿcᵐ}` and `L₂ = {aᵐbⁿcⁿ}` (each: a BNF grammar + an exact-generation
+   proof, i.e. soundness + completeness), with `L₁ ∩ L₂ = {aⁿbⁿcⁿ}` discharged by
+   `anbncn_not_cfl`. This is mechanical grammar-construction plumbing on top of the
+   verified crux.
+
+Plan: land it as its own follow-up PR (incremental, same as the pumping lemma).
+
+## CI notes
+
+On PR #106, the genuinely-relevant checks are green (Trusted-base reduction
+policy; the Lean/Coq compile gates). Three checks are red but are **pre-existing
+infrastructure failures unrelated to these proofs**, and every prior merged PR
+(#102–#105) carried them too:
+
+- **Licence consistency** — root `LICENSE` SPDX mismatch.
+- **Workflow security linter** — a `trufflehog@main` unpinned-action finding.
+- **Hypatia Neurosymbolic Analysis** — scanner infrastructure.
+
+## Moving this session to desktop
+
+Per the Claude Code docs, use **teleport** to carry the conversation context +
+branch + uncommitted changes from web into the local CLI / desktop app:
+`claude --teleport <session-id>` (one-way: web → local). See
+<https://code.claude.com/docs/en/claude-code-on-the-web>. Even without it, the
+branch and PR #106 hold all the work.
@@ -332,8 +332,12 @@ The binding power comparison ensures this:
 > — 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
+> decomposition with `1 ≤ |vx|` and `|vwx| ≤ 2^(card+1)`). As its canonical
+> application, the same file machine-checks **`aⁿbⁿcⁿ ∉ CFL`** (`anbncn_not_cfl`) —
+> the standard witness that the CFLs are not closed under ∩ / ¬ (pump down to
+> `i = 0` ⇒ equal letter-counts ⇒ the window spans `a`…`c` ⇒ `|vwx| > p`). The
+> remaining §7.3 *non*-closure step is purely the two witness-grammar constructions
+> `{aⁿbⁿcᵐ}`, `{aᵐbⁿcⁿ}`; status in
 > `../verification/GRAMMAR-PROOF-INVENTORY.md`.
 
 ### 7.1 Chomsky Hierarchy Position

@@ -72,7 +72,8 @@ reach here, with reason).
 | 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.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 |
+| T7.0b | `aⁿbⁿcⁿ ∉ CFL` (canonical non-CFL) | ✅ done from scratch | **Ext** | `WokeGrammarPumping.lean`: `anbncn_not_cfl` via `cfl_pumping` (pump `i=0` ⇒ equal counts ⇒ window spans `a`…`c` ⇒ `|vwx|>p`); positional core `prefix_pure`/`abc_window`; classical kernel constants only | MACHINE-CHECKED |
+| T7.3b | §7.3 CFL **not** closed under ∩, ¬ | ⚠️ canonical witness done; wrapper remaining | **P6** | `aⁿbⁿcⁿ ∉ CFL` (T7.0b) is the crux and is proved; remaining: the two witness CFLs `{aⁿbⁿcᵐ}`,`{aᵐbⁿcⁿ}` (BNF grammars + exact generation) whose intersection is `aⁿbⁿcⁿ` | IN PROGRESS |
 
 ## Priority order (execution)
 
@@ -186,11 +187,42 @@ identical" per `AUDIT.md`.)
   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.
+- **`aⁿbⁿcⁿ ∉ CFL` — DONE** (`WokeGrammarPumping.lean`, `anbncn_not_cfl`): the
+  canonical non-context-free language, the crux of any ∩/¬ non-closure argument.
+  `IsCFL` is defined finiteness-aware (an ε-free BNF grammar with an `enum`/`card`
+  nonterminal bound, matching `cfl_pumping`; the relation-based `IsCFL` used for
+  *positive* closure is too permissive here — an infinite nonterminal type could
+  "generate" `aⁿbⁿcⁿ`). Proof: apply `cfl_pumping` to `aᵖbᵖcᵖ`; pumping down to
+  `i = 0` forces `count_a = count_b = count_c` in the deleted part, so the pumped
+  window contains an `a` and a `c`; the positional core (`prefix_pure` by induction
+  on the prefix, `abc_window`) then gives `|vwx| > p`, contradicting `|vwx| ≤ p`.
+- **§7.3 *non-closure* under ∩ / ¬** — the remaining wrapper. With `aⁿbⁿcⁿ ∉ CFL`
+  proved, the explicit statement follows from the two witness CFLs `{aⁿbⁿcᵐ}` and
+  `{aᵐbⁿcⁿ}` (whose intersection is `aⁿbⁿcⁿ`); each needs a BNF grammar plus an
+  exact-generation (soundness + completeness) proof — mechanical grammar-construction
+  plumbing on top of the verified crux.
+
+## Axiom audit (`#print axioms`, verified in-toolchain)
+
+Kernel-dependency printout for the headline results in `WokeGrammarPumping.lean`
+(Lean 4.30.0). Only the standard classical constants appear — no `sorryAx`, no
+project-specific constants:
+
+| Theorem | Kernel dependencies |
+|---|---|
+| `yield_bound` | `propext`, `Quot.sound` |
+| `ht_descend` | `propext`, `Quot.sound` |
+| `nodeNT_add` | `propext`, `Classical.choice`, `Quot.sound` |
+| `descend_sibling_nonempty` | `propext`, `Quot.sound` |
+| `cfl_pumping` | `propext`, `Classical.choice`, `Quot.sound` |
+| `prefix_pure` | `propext` |
+| `abc_window` | `propext`, `Quot.sound` |
+| `anbncn_not_cfl` | `propext`, `Classical.choice`, `Quot.sound` |
+
+`Classical.choice` enters only through the finite `pigeon`hole's case split; the
+rest are the kernel constants Mathlib itself rests on. The other files' headline
+results sit on the same or a smaller base (`WokeGrammarCFL.lean` is `propext`-only;
+`WokeGrammarStructure`'s `no_left_recursion` is fully constant-free).
 
 ## Status