[hyperpolymath]

Closes the last open item from grammar-proofs.md §7.3 (positive direction):
the class of context-free languages is closed under union, concatenation, and
Kleene star — machine-checked from scratch (no Mathlib).

WokeGrammarCFL.lean (Lean 4.30.0, CI-gated, sorry-free, propext-only)

• A general CFG: a production relation P : N → List (N ⊕ T) → Prop with a mutual
  derivation relation Gen/GenL; IsCFL L := ∃ grammar generating exactly L.
• One reusable core lemma embGen_iff: embedding a grammar's nonterminals
  into a larger disjoint grammar preserves the generated language. This is the
  load-bearing result — a lift direction plus a generalized-index structural
  reflection (the index is generalized to a variable + equation so Lean's mutual
  brecOn accepts the recursion).
• The three closures as grammar constructions, each with a full language-equality
  proof:
  • cfl_union — none → S1 \| S2
  • cfl_concat — none → S1 S2
  • cfl_star — none → ε \| S1 S (the self-recursive one; handled via a mutual
    Gen/GenL forward pass)
  • cfl_single — {[t]} is context-free (non-vacuity).

#print axioms → propext only. The WokeLang surface grammar is context-free, so
it inhabits this class and these operations apply to it.

Still scoped (honestly)

§7.3 non-closure under intersection / complement needs the pumping lemma for
CFLs (e.g. to show aⁿbⁿcⁿ is not context-free) — a separate larger development,
recorded in GRAMMAR-PROOF-INVENTORY.md rather than stubbed.

Status of the whole grammar-proofs effort

With this PR, every prose claim in grammar-proofs.md is now machine-checked
except the §7.3 negative-closure results: parser metatheory (Lean + Coq),
no-left-recursion (+ the guard-pattern bug found), lexer munch/priority,
LL(1)✗/LL(2)✓, §7.1 not-regular, and §7.3 positive closure.

🤖 Generated with Claude Code

https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL

---

Generated by Claude Code