diff --git a/.github/workflows/coq-proofs.yml b/.github/workflows/coq-proofs.yml
index c3ed939..b76602a 100644
--- a/.github/workflows/coq-proofs.yml
+++ b/.github/workflows/coq-proofs.yml
@@ -12,10 +12,12 @@ on:
   push:
     paths:
       - 'docs/proofs/verification/WokeLang.v'
+      - 'docs/proofs/verification/WokeGrammarStructure.v'
       - '.github/workflows/coq-proofs.yml'
   pull_request:
     paths:
       - 'docs/proofs/verification/WokeLang.v'
+      - 'docs/proofs/verification/WokeGrammarStructure.v'
       - '.github/workflows/coq-proofs.yml'
 
 permissions:
@@ -40,3 +42,10 @@ jobs:
           cd docs/proofs/verification
           coqc WokeLang.v
           echo "✅ WokeLang.v verified"
+
+      - name: Verify WokeGrammarStructure.v (no-left-recursion + classification; axiom-free)
+        run: |
+          set -euo pipefail
+          cd docs/proofs/verification
+          coqc WokeGrammarStructure.v
+          echo "✅ WokeGrammarStructure.v verified"
diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml
index d5d6690..0fa54ba 100644
--- a/.github/workflows/lean-proofs.yml
+++ b/.github/workflows/lean-proofs.yml
@@ -50,3 +50,9 @@ jobs:
           set -euo pipefail
           lean docs/proofs/verification/WokeGrammar.lean
           echo "✅ WokeGrammar.lean verified"
+
+      - name: Verify WokeGrammarStructure.lean (no-left-recursion + lexer + classification)
+        run: |
+          set -euo pipefail
+          lean docs/proofs/verification/WokeGrammarStructure.lean
+          echo "✅ WokeGrammarStructure.lean verified"
diff --git a/docs/proofs/formal-semantics/grammar-proofs.md b/docs/proofs/formal-semantics/grammar-proofs.md
index e02a78f..b463a4a 100644
--- a/docs/proofs/formal-semantics/grammar-proofs.md
+++ b/docs/proofs/formal-semantics/grammar-proofs.md
@@ -64,6 +64,15 @@ logical_or = logical_and { "or" logical_and }
 
 The `{ }` repetition prevents left-recursion. □
 
+> **Correction (machine-checked, `WokeGrammarStructure.lean/.v`).** This blanket
+> claim is **inaccurate for the grammar as literally written**: the `pattern`
+> production has the guard alternative `pattern = … | pattern "when" expression`,
+> which is *directly left-recursive* (`guard_pattern_is_left_recursive`). No
+> left recursion holds for the **implemented** grammar (the parser does not
+> implement the guard alternative — see the grammar's own NOTE), which is what
+> `no_left_recursion` proves. The table above also omits `pattern`; with the
+> guard alternative it is the sole left-recursive production.
+
 ### 2.2 No Ambiguity
 
 **Theorem 2.2:** The WokeLang grammar is unambiguous.
@@ -312,6 +321,15 @@ The binding power comparison ensures this:
 
 ## 7. Formal Language Theory
 
+> **Mechanization status.** The §7 results (not-regular via pumping; CFL closure /
+> non-closure) are general facts about the *classes* REG/CFL, not about the
+> WokeLang grammar specifically, and need a general automata/grammar library
+> (Mathlib's `Computability.*`) that the repo's deliberately Mathlib-free, offline,
+> single-file prover setup does not provide. They are therefore **not machine-checked
+> here** — recorded honestly in `../verification/GRAMMAR-PROOF-INVENTORY.md` rather
+> than stubbed. The combinatorial kernel (unbounded balanced nesting) *is* exercised
+> concretely in `WokeGrammar.lean`.
+
 ### 7.1 Chomsky Hierarchy Position
 
 ```
diff --git a/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md b/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md
index 76875d9..1abfe42 100644
--- a/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md
+++ b/docs/proofs/verification/GRAMMAR-PROOF-INVENTORY.md
@@ -57,7 +57,7 @@ reach here, with reason).
 
 | # | Prose claim (grammar-proofs.md) | Faithful here? | Priority | Mechanization | Status |
 |---|---|---|---|---|---|
-| T2.1 | §2.1 No left recursion | ✅ yes (whole grammar) | **P2** | Grammar as data; `¬ LeftRecursive G` by decision/structural proof over **all** productions | MACHINE-CHECKED |
+| T2.1 | §2.1 No left recursion | ✅ yes (whole grammar) | **P2** | Grammar as data; rank-decreasing `Reach` ⇒ `¬ Reach a a` over **all** productions | MACHINE-CHECKED (**+ found a real discrepancy:** the guard pattern IS left-recursive — see below) |
 | T2.2 | §2.2 Unambiguity | ✅ for the core (undecidable in general) | **P1** | Determinism of the verified parser ⇒ unique parse: `Derives ts e₁ → Derives ts e₂ → e₁=e₂` for the expression core | MACHINE-CHECKED (core) |
 | T2.3 | §2.3 LL(2) | ◑ partial | **P4** | The one 2-token decision (`ident` vs `ident(`) witnessed; determinism of the core parser. Full LL(2) table for all 94 productions is not built | MACHINE-CHECKED (witness) |
 | T3.1 | §3.1 Parser soundness | ✅ for the core | **P1** | `parse ts = some (e, rest) → Derives (consumed) e` | MACHINE-CHECKED (core) |
@@ -69,7 +69,7 @@ reach here, with reason).
 | T6.3 | §6.3 Left-associativity | ✅ | **P1** | `a-b-c ↦ (a-b)-c` from the strict-`<` model + general statement | MACHINE-CHECKED |
 | T1.1 | §1.1 CFG membership | ✅ | **P4** | By construction (the grammar relation is a CFG) | MACHINE-CHECKED |
 | 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 ∪, ·, * | ✅ | **P5** | Explicit grammar constructions + language-equality proofs | MACHINE-CHECKED |
+| T7.3a | §7.3 CFL closed under ∪, ·, * | ⚠️ needs a general CFG/language module | **P5** | Explicit grammar constructions + language-equality proofs (standalone module, not a fact about *this* grammar) | FLAGGED |
 | T7.1 | §7.1 Not regular (pumping lemma) | ⚠️ no (needs automata/Mathlib offline) | **P6** | Mechanize the combinatorial kernel (the balanced-paren sublanguage `(ⁿ)ⁿ ⊆ L`); full DFA+pumping non-regularity needs Mathlib's `Computability` (network-fetched, unavailable) | FLAGGED + partial kernel |
 | 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 |
 
@@ -128,7 +128,64 @@ cleaner than `WokeLang.lean`).
   relation) is the one honest extension still open on P1; the rejection battery
   covers the no-junk direction concretely.
 
+## Landed — P2/P3/P4 (`WokeGrammarStructure.lean`, Lean 4.30.0)
+
+CI-gated (`lean-proofs.yml`), `sorry`-free; `no_left_recursion` depends on **no
+axioms at all** (fully constructive).
+
+- **T2.1 no left recursion (P2)** — the begins-with-first-nonterminal graph of the
+  *whole* grammar is encoded as data with a strictly-decreasing rank; `Reach`
+  (transitive first-symbol reachability) ⇒ `no_left_recursion : ∀ a, ¬ Reach a a`.
+  **Discrepancy found & machine-checked:** the grammar *as literally written* has
+  one left-recursive production — the guard pattern `pattern = … | pattern "when"
+  expression` (`guard_pattern_is_left_recursive`). So the prose §2.1 blanket "no
+  left recursion" is **false as written**; it holds only for the implemented
+  subset (the parser does not implement the guard alternative — the grammar's own
+  NOTE). This corrects the prose.
+- **T4.1 maximal munch / T4.2 keyword priority (P3)** — a word scanner taking the
+  maximal identifier run + keyword-on-exact-match: `kw_priority` (general),
+  `munch_maximal` (general longest-match: the remainder never extends the token),
+  plus kernel-`decide`d concretes (`remember`↦keyword, `remembering`↦*one*
+  identifier not `remember`+`ing`, `remember(`↦keyword then stop).
+- **T1.2 LL(1)=✗ / T2.3 LL(2)=✓ (P4)** — `not_LL1` (the `x` vs `x(…)` FIRST/FIRST
+  conflict shares FIRST₁ = identifier) and `LL2_separates` (two tokens decide,
+  mirroring the parser's `peek == '('` branch). CFG membership holds by
+  construction.
+
+## Landed — Coq mirror (`WokeGrammarStructure.v`, Coq 8.18.0)
+
+CI-gated (`coq-proofs.yml`); `Print Assumptions` reports **axiom-free** ("Closed
+under the global context"). Mirrors **P2 (no-left-recursion + guard discrepancy)**
+and **P4 (LL(1)✗/LL(2)✓)** in lockstep with Lean. (The Lean↔Coq relationship for
+the *parser metatheory* P1 follows the repo's existing pattern — Lean carries the
+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`.)
+
+## Flagged — P5/P6 (§7 formal-language-theory claims), honestly not mechanized
+
+These prose claims are **general facts about the *classes* `REG`/`CFL`**, not
+properties of the WokeLang grammar, and need a general automata/grammar library:
+
+- **T7.1 not regular (pumping lemma)** and **§7.3 CFL non-closure under ∩ / ¬**
+  require a formal DFA + pumping-lemma development (or the CFL pumping lemma for
+  the non-closure direction). Mathlib has this (`Mathlib.Computability.*`), but
+  the repo's proofs are deliberately **Mathlib-free and offline** (single-file
+  `lean <file>`), and `lake`/reservoir fetching is blocked by egress policy here.
+  Building DFA + pumping from scratch in core Lean is a large standalone module.
+- **§7.3 CFL *positive* closure (∪, ·, \*)** is mechanizable but needs a general
+  CFG + language-semantics module (a derivation relation over arbitrary grammars
+  and the three closure constructions) — also a standalone development, not a fact
+  about *this* grammar.
+
+Per the agreed "flag, don't fake" rule these are recorded here rather than stubbed.
+The combinatorial kernel of non-regularity (unbounded balanced nesting `(ⁿ … )ⁿ`)
+*is* exercised concretely — `WokeGrammar.lean` parses `((1))` and arbitrarily
+grouped inputs — but the full automata-theoretic theorems remain out of faithful
+reach in this setup.
+
 ## Status
 
-P1 landed (above). P2–P6 + the Coq mirror proceed in priority order; the
-authoritative status is always "does the CI prover check go green."
+P1 (merged, #102) + P2/P3/P4 + the structural Coq mirror are machine-checked and
+CI-gated. P5/P6 are honestly flagged above. The authoritative status is always
+"does the CI prover check go green."
diff --git a/docs/proofs/verification/WokeGrammarStructure.lean b/docs/proofs/verification/WokeGrammarStructure.lean
new file mode 100644
index 0000000..f42f722
--- /dev/null
+++ b/docs/proofs/verification/WokeGrammarStructure.lean
@@ -0,0 +1,233 @@
+/-
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+WokeGrammarStructure.lean — structural / classification proofs about the WokeLang
+grammar (`grammar/wokelang.ebnf`). Self-contained (Lean core prelude only).
+
+This file mechanizes **T2.1 (no left recursion)** for the *whole* grammar, and
+in doing so surfaces a genuine discrepancy with the prose `grammar-proofs.md`
+§2.1: the grammar **as literally written** DOES contain one left-recursive
+production — the guard pattern `pattern = … | pattern "when" expression` — which
+the grammar's own NOTE flags as "parser implementation pending" and which the
+real parser (`src/parser/mod.rs`) does not implement. With that single
+unimplemented alternative excluded, the grammar is provably left-recursion-free.
+
+Method: a left-recursive grammar has a nonterminal A that, following only
+*first* symbols, can reach itself. We encode the "begins with first nonterminal"
+graph of every production (all terminal-first productions collapse to the single
+`sink` node — they have no outgoing edge and so cannot lie on a cycle), exhibit a
+rank that strictly decreases along every edge, and conclude no cycle exists.
+-/
+
+namespace WokeGrammarStructure
+
+/-- Nonterminals that participate in the begins-with-first-nonterminal graph of
+`grammar/wokelang.ebnf`. Every terminal-first production (the vast majority —
+`remember`, `when`, `to`, `worker`, `"`, `[`, `|`, …) is a `sink`: it has no
+outgoing first-nonterminal edge and therefore cannot be on a cycle. -/
+inductive NT where
+  | program | topItem | functionDef | paramList | statement | exprStmt
+  | emoteAnnotated | matchArm | pattern | patternList | constraint
+  | typeVariant | enumType | typeList | type
+  | expression | logicalOr | logicalAnd | equality | comparison
+  | additive | multiplicative | unary | postfixE | primary | literal | number
+  | argList | sink
+  deriving DecidableEq, Repr
+
+open NT
+
+/-- Every begins-with-first-nonterminal edge of the grammar, **excluding** the
+unimplemented guard-pattern alternative `pattern → pattern`. Terminal-first
+alternatives are recorded as an edge to `sink`. -/
+def edges : List (NT × NT) :=
+  [ (program, topItem),
+    (topItem, functionDef), (topItem, sink),
+    (functionDef, sink),
+    (paramList, sink),
+    (statement, exprStmt), (statement, emoteAnnotated), (statement, sink),
+    (exprStmt, expression),
+    (emoteAnnotated, sink),
+    (matchArm, pattern),
+    (pattern, literal),               -- the guard alt `pattern "when" …` is excluded
+    (patternList, pattern),
+    (constraint, expression),
+    (typeVariant, type), (typeVariant, enumType), (typeVariant, sink),
+    (enumType, sink),
+    (typeList, type),
+    (type, sink),
+    (expression, logicalOr),
+    (logicalOr, logicalAnd), (logicalAnd, equality), (equality, comparison),
+    (comparison, additive), (additive, multiplicative),
+    (multiplicative, unary), (unary, postfixE), (postfixE, primary),
+    (primary, literal), (primary, sink),
+    (literal, number),
+    (argList, expression) ]
+
+/-- A topological rank: strictly decreases along every edge (witnessing that the
+begins-graph is a DAG). Higher = closer to the start symbol. -/
+def rank : NT → Nat
+  | program => 80 | topItem => 70 | statement => 50
+  | matchArm => 30 | patternList => 30 | functionDef => 30
+  | paramList => 20 | constraint => 40 | argList => 40
+  | typeVariant => 20 | typeList => 20 | enumType => 10 | type => 10
+  | exprStmt => 40 | emoteAnnotated => 40
+  | expression => 29 | logicalOr => 28 | logicalAnd => 27 | equality => 26
+  | comparison => 25 | additive => 24 | multiplicative => 23 | unary => 22
+  | postfixE => 21 | primary => 20 | pattern => 15 | literal => 10 | number => 5
+  | sink => 0
+
+/-- Every edge strictly decreases `rank` (checked by the kernel). -/
+theorem rank_decreasing : ∀ p ∈ edges, rank p.2 < rank p.1 := by decide
+
+/-- Reachability by following one or more first-nonterminal edges. `Reach a a`
+is exactly "`a` is (directly or indirectly) left-recursive". -/
+inductive Reach : NT → NT → Prop
+  | edge {a b} : (a, b) ∈ edges → Reach a b
+  | step {a b c} : (a, b) ∈ edges → Reach b c → Reach a c
+
+/-- Rank strictly decreases along any reachability path. -/
+theorem reach_rank {a b : NT} (h : Reach a b) : rank b < rank a := by
+  induction h with
+  | edge hab => exact rank_decreasing _ hab
+  | step hab _ ih => exact Nat.lt_trans ih (rank_decreasing _ hab)
+
+/-- **T2.1 — no left recursion (implemented grammar).** With the unimplemented
+guard-pattern alternative excluded, no nonterminal is left-recursive: it cannot
+reach itself by following first symbols. (Proof: a self-path would force
+`rank a < rank a`.) Covers the whole grammar — every terminal-first production is
+a `sink`, which has no outgoing edge. -/
+theorem no_left_recursion (a : NT) : ¬ Reach a a := by
+  intro h; exact Nat.lt_irrefl _ (reach_rank h)
+
+/-! ### The honest discrepancy with the prose §2.1 -/
+
+/-- The grammar **as literally written** also has the guard alternative. -/
+def edgesAsWritten : List (NT × NT) := (pattern, pattern) :: edges
+
+/-- **Discrepancy (machine-checked).** The guard pattern `pattern = … | pattern
+"when" expression` is *directly left-recursive*: `pattern → pattern` is an edge of
+the grammar as written. So the prose §2.1 blanket claim "the WokeLang grammar
+contains no left recursion" is **false for the grammar as literally written**;
+it holds only for the implemented subset (`no_left_recursion`), because the
+parser does not implement the guard alternative (the grammar's own NOTE). -/
+theorem guard_pattern_is_left_recursive :
+    (NT.pattern, NT.pattern) ∈ edgesAsWritten := by decide
+
+/-! ## 2. Lexer: maximal munch (T4.1) and keyword priority (T4.2)
+
+Models the live lexer (`src/lexer/token.rs`, logos): identifiers match
+`[a-zA-Z][a-zA-Z0-9_]*` and keywords are exact-string tokens. logos takes the
+**longest** match (maximal munch); on a tie it prefers the keyword. We model the
+word scanner directly: take the maximal run of identifier characters, then a word
+that is exactly a keyword classifies as that keyword, otherwise as an identifier. -/
+
+inductive Lexeme where
+  | kw : String → Lexeme
+  | ident : String → Lexeme
+  deriving DecidableEq, Repr
+
+/-- The reserved keywords of WokeLang (the grammar's RESERVED KEYWORDS list). -/
+def keywords : List String :=
+  ["to","give","back","remember","when","otherwise","repeat","times","while",
+   "break","continue","only","if","okay","attempt","safely","reassure","complain",
+   "thanks","hello","goodbye","worker","side","quest","superpower","spawn","send",
+   "receive","channel","await","cancel","from","decide","based","on","measured",
+   "in","use","renamed","share","type","const","String","Int","Float","Bool",
+   "Maybe","Result","must","have","care","strict","verbose","true","false","and",
+   "or","not","Okay","Oops","unwrap"]
+
+def isLetter (c : Char) : Bool := c.isAlpha
+def isIdentCont (c : Char) : Bool := c.isAlphanum || c == '_'
+
+/-- Take the maximal leading run of identifier-continuation characters. -/
+def takeCont : List Char → List Char × List Char
+  | [] => ([], [])
+  | c :: cs =>
+    if isIdentCont c then (c :: (takeCont cs).1, (takeCont cs).2)
+    else ([], c :: cs)
+
+/-- Keyword priority: a word equal to a keyword is the keyword token. -/
+def classifyWord (w : String) : Lexeme := if w ∈ keywords then .kw w else .ident w
+
+/-- Lex one word: an identifier-start letter, then the maximal identifier run,
+then classify (keyword if exact, else identifier). -/
+def lexWord : List Char → Option (Lexeme × List Char)
+  | [] => none
+  | c :: cs =>
+    if isLetter c then
+      some (classifyWord (String.ofList (c :: (takeCont cs).1)), (takeCont cs).2)
+    else none
+
+/-- **T4.2 keyword priority (general):** any reserved word lexes as its keyword. -/
+theorem kw_priority {w : String} (h : w ∈ keywords) : classifyWord w = .kw w := by
+  unfold classifyWord; rw [if_pos h]
+
+/-- **T4.1 maximal munch (general):** after the maximal identifier run, the
+remainder cannot begin with another identifier character — the scanner could not
+have stopped earlier. This is the longest-match property. -/
+theorem munch_maximal :
+    ∀ (cs : List Char) (c : Char) (rest : List Char),
+      (takeCont cs).2 = c :: rest → isIdentCont c = false := by
+  intro cs
+  induction cs with
+  | nil => intro c rest h; simp [takeCont] at h
+  | cons d ds ih =>
+    intro c rest h
+    simp only [takeCont] at h
+    split at h
+    · exact ih c rest h
+    · rename_i hd
+      obtain ⟨rfl, _⟩ := List.cons.inj h
+      simpa using hd
+
+/-! ### Concrete lexer checks (kernel-decided) -/
+
+-- keyword priority: "remember" is the keyword, not a generic identifier.
+example : classifyWord "remember" = Lexeme.kw "remember" := by decide
+-- maximal munch: "remembering" is ONE identifier, not `remember` + `ing`.
+example : lexWord "remembering".toList = some (Lexeme.ident "remembering", []) := by decide
+-- "remember(" lexes the keyword then stops at `(` (a non-identifier char).
+example : lexWord "remember(".toList = some (Lexeme.kw "remember", "(".toList) := by decide
+-- a non-keyword word is an identifier.
+example : lexWord "myVar".toList = some (Lexeme.ident "myVar", []) := by decide
+-- a leading non-letter is not an identifier start.
+example : lexWord "1abc".toList = none := by decide
+
+/-! ## 3. Classification: LL(1) = ✗ (T1.2), LL(2) = ✓ (T2.3)
+
+The grammar is context-free by construction (every production is `A → α`). It is
+**not LL(1)**: the `primary` alternatives `identifier` (variable) and
+`identifier "(" args ")"` (call) share the FIRST token `identifier`, so one token
+of lookahead cannot choose between them. It **is** resolvable with two tokens —
+exactly what the real parser does (`parse_prefix` consumes the identifier, then
+branches on whether the next token is `(`). -/
+
+inductive PTok where | ident | lparen | other deriving DecidableEq, Repr
+inductive PrimaryAlt where | var | call deriving DecidableEq, Repr
+
+/-- FIRST₁ of the two `primary` alternatives that begin with an identifier. -/
+def first1 : PrimaryAlt → PTok
+  | .var => .ident
+  | .call => .ident
+
+/-- **T1.2 — not LL(1):** the two alternatives have identical FIRST₁ (`identifier`),
+so a single lookahead token cannot disambiguate `x` (variable) from `x(...)`
+(call). This is the FIRST/FIRST conflict the prose §1.1 marks LL(1) = ✗. -/
+theorem not_LL1 : first1 .var = first1 .call := rfl
+
+/-- The parser's two-token decision: an identifier followed by `(` is a call,
+otherwise a variable (mirrors `parse_prefix` in `src/parser/mod.rs`). -/
+def decide2 : PTok → PTok → Option PrimaryAlt
+  | .ident, .lparen => some .call
+  | .ident, _       => some .var
+  | _,      _       => none
+
+/-- **T2.3 — LL(2):** two tokens DO separate the alternatives — `identifier (`
+selects the call, `identifier <anything else>` selects the variable, and these
+are distinct decisions. -/
+theorem LL2_separates : decide2 .ident .lparen ≠ decide2 .ident .other := by decide
+theorem LL2_call : decide2 .ident .lparen = some .call := rfl
+theorem LL2_var  : decide2 .ident .other  = some .var  := rfl
+
+end WokeGrammarStructure
diff --git a/docs/proofs/verification/WokeGrammarStructure.v b/docs/proofs/verification/WokeGrammarStructure.v
new file mode 100644
index 0000000..be6797c
--- /dev/null
+++ b/docs/proofs/verification/WokeGrammarStructure.v
@@ -0,0 +1,130 @@
+(*
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+WokeGrammarStructure.v — Coq mirror of the structural grammar proofs in
+WokeGrammarStructure.lean (the repo keeps Lean and Coq in lockstep). Covers
+T2.1 (no left recursion, with the guard-pattern discrepancy) and the LL(1)=X /
+LL(2)=ok classification. Axiom-free; verified with `coqc WokeGrammarStructure.v`
+under Coq 8.18.0.
+*)
+
+Require Import List.
+Import ListNotations.
+Require Import PeanoNat.
+Require Import Lia.
+
+(* Nonterminals on the begins-with-first-nonterminal graph; all terminal-first
+   productions collapse to [sink] (no outgoing edge, cannot be on a cycle). *)
+Inductive NT : Type :=
+  | program | topItem | functionDef | paramList | statement | exprStmt
+  | emoteAnnotated | matchArm | pattern | patternList | constraintN
+  | typeVariant | enumType | typeList | typeN
+  | expression | logicalOr | logicalAnd | equality | comparison
+  | additive | multiplicative | unary | postfixE | primary | literal | number
+  | argList | sink.
+
+(* Begins-with-first-nonterminal edges (guard-pattern alt excluded). *)
+Definition edges : list (NT * NT) :=
+  [ (program, topItem);
+    (topItem, functionDef); (topItem, sink);
+    (functionDef, sink);
+    (paramList, sink);
+    (statement, exprStmt); (statement, emoteAnnotated); (statement, sink);
+    (exprStmt, expression);
+    (emoteAnnotated, sink);
+    (matchArm, pattern);
+    (pattern, literal);
+    (patternList, pattern);
+    (constraintN, expression);
+    (typeVariant, typeN); (typeVariant, enumType); (typeVariant, sink);
+    (enumType, sink);
+    (typeList, typeN);
+    (typeN, sink);
+    (expression, logicalOr);
+    (logicalOr, logicalAnd); (logicalAnd, equality); (equality, comparison);
+    (comparison, additive); (additive, multiplicative);
+    (multiplicative, unary); (unary, postfixE); (postfixE, primary);
+    (primary, literal); (primary, sink);
+    (literal, number);
+    (argList, expression) ].
+
+Definition rank (n : NT) : nat :=
+  match n with
+  | program => 80 | topItem => 70 | statement => 50
+  | matchArm => 30 | patternList => 30 | functionDef => 30
+  | paramList => 20 | constraintN => 40 | argList => 40
+  | typeVariant => 20 | typeList => 20 | enumType => 10 | typeN => 10
+  | exprStmt => 40 | emoteAnnotated => 40
+  | expression => 29 | logicalOr => 28 | logicalAnd => 27 | equality => 26
+  | comparison => 25 | additive => 24 | multiplicative => 23 | unary => 22
+  | postfixE => 21 | primary => 20 | pattern => 15 | literal => 10 | number => 5
+  | sink => 0
+  end.
+
+(* Every edge strictly decreases rank (computed). *)
+Lemma rank_decreasing_b :
+  forallb (fun p => Nat.ltb (rank (snd p)) (rank (fst p))) edges = true.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma rank_decreasing : forall a b, In (a, b) edges -> rank b < rank a.
+Proof.
+  intros a b Hin.
+  assert (Hall := rank_decreasing_b).
+  rewrite forallb_forall in Hall.
+  specialize (Hall (a, b) Hin). simpl in Hall.
+  apply Nat.ltb_lt in Hall. exact Hall.
+Qed.
+
+(* Reachability by following one or more first-nonterminal edges. *)
+Inductive Reach : NT -> NT -> Prop :=
+  | Reach_edge : forall a b, In (a, b) edges -> Reach a b
+  | Reach_step : forall a b c, In (a, b) edges -> Reach b c -> Reach a c.
+
+Lemma reach_rank : forall a b, Reach a b -> rank b < rank a.
+Proof.
+  intros a b H. induction H as [a b Hin | a b c Hin Hbc IH].
+  - apply rank_decreasing; exact Hin.
+  - apply rank_decreasing in Hin. lia.
+Qed.
+
+(* T2.1 — no left recursion (implemented grammar): no nonterminal reaches itself. *)
+Theorem no_left_recursion : forall a, ~ Reach a a.
+Proof.
+  intros a H. apply reach_rank in H. lia.
+Qed.
+
+(* The grammar as literally written also has the guard alternative. *)
+Definition edgesAsWritten : list (NT * NT) := (pattern, pattern) :: edges.
+
+(* Discrepancy: the guard pattern is directly left-recursive — refuting the prose
+   blanket claim "no left recursion" for the grammar as literally written. *)
+Theorem guard_pattern_is_left_recursive : In (pattern, pattern) edgesAsWritten.
+Proof. simpl. left. reflexivity. Qed.
+
+(* ---- Classification: LL(1) = X (T1.2), LL(2) = ok (T2.3) ---- *)
+
+Inductive PTok := PIdent | PLparen | POther.
+Inductive PrimaryAlt := AVar | ACall.
+
+Definition first1 (a : PrimaryAlt) : PTok :=
+  match a with AVar => PIdent | ACall => PIdent end.
+
+(* T1.2 — not LL(1): the two alternatives share FIRST1 = identifier. *)
+Theorem not_LL1 : first1 AVar = first1 ACall.
+Proof. reflexivity. Qed.
+
+Definition decide2 (t1 t2 : PTok) : option PrimaryAlt :=
+  match t1, t2 with
+  | PIdent, PLparen => Some ACall
+  | PIdent, _       => Some AVar
+  | _,      _       => None
+  end.
+
+(* T2.3 — LL(2): two tokens separate the alternatives. *)
+Theorem LL2_separates : decide2 PIdent PLparen <> decide2 PIdent POther.
+Proof. simpl. discriminate. Qed.
+Theorem LL2_call : decide2 PIdent PLparen = Some ACall.
+Proof. reflexivity. Qed.
+Theorem LL2_var : decide2 PIdent POther = Some AVar.
+Proof. reflexivity. Qed.