=== AGENTS.md
   49:   checked-in tool is `Probe/forbidden_tokens.py` (tracks `/-` `-/` nesting depth, strips `--`
   52:   `python3 Probe/forbidden_tokens.py <file.lean> ...` with an explicit file list — it does not
  379: 2. `python3 Probe/forbidden_tokens.py <your files>` reports `sorry=0 admit=0 axiom=0
=== HANDOVER.md
   13:   statement-only deliveries of batch 229-A (see the next bullet): `python3 Probe/forbidden_tokens.py <files>`
   14:   reports all zeros for every other module, and every public declaration of the recent modules carries a
   16:   --- except the declarations that consume the two holes, whose guards print `sorryAx` on purpose.
  142: * `python3 Probe/forbidden_tokens.py <explicit file list>` -> all zeros.
  144:   printer wraps at 120 chars, name-dependently).  MEASURED TRAP: an elaboration failure becomes `sorryAx` and the
=== README.md
    8: Lean 4.33.1, Mathlib pinned at `db584cd6d46c92f209a44c0f1c829460d327499d`. **No added `axiom`,
  156: | `Definitions/MMLevelTwo.lean` | The level-2 half of the paper's section 11: `E8` as `D8` plus the half-integral coset, `MM.E8.IsLattice`, `MM.E8.normSq` (`8 ∣ Σ yᵢ²` is what makes the divi
  218: footprint printed *with* `sorryAx`, so the hole cannot hide behind a passing build:
  226: `theorem889_delta`, `remark8811_res_z0`/`_res_z1`, `remark8812_res_z2`) carry `sorryAx` in their
  245: > `Definitions/MMLevelTwo.lean` are unchanged and are now **corollaries**; that file reads `sorry=0`.
  259: `moonshine_conjecture` unguarded, so that `sorryAx` stays visible rather than being hidden behind a
=== ROADMAP.md
  285: > `forbidden_tokens` 0/0/0/0, every guarded declaration on `[propext, Classical.choice, Quot.sound]`
 1252: > `key_injective` only *elaborated* on top of an error-recovered `sorryAx` dependency — the evidence file
 1254: > line is `'MM.Attempt2.key_injective' depends on axioms: [propext, sorryAx, Classical.choice,
 1268: >    ever *elaborated* on a `sorryAx` dependency** — `Probe/LpAx1.lean` still reproduces
 1269: >    `'…key_injective' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]`.  So the
 1614: > three `--- OK ---` lines, exit 0; `forbidden_tokens.py` clean on all three, exit 0; `FinalCheck.lean`
 2098: >   16/16 `--- OK ---`, exit 0; `Probe/forbidden_tokens.py` → `sorry=0 admit=0 axiom=0
 2370: `Probe/forbidden_tokens.py` at `sorry=0 admit=0 axiom=0 native_decide=0`; all 9 in-file guards
 2371: matched verbatim, every footprint `[propext, Classical.choice, Quot.sound]`, none touching `sorryAx`.
 2380:    `[propext, sorryAx, Classical.choice, Quot.sound]`, i.e. an *unproved* declaration with no `sorry`
 2381:    anywhere in the file text.  `Probe/forbidden_tokens.py` passes such a file; only the
 2416: `python3 Scratch2/forbidden_tokens.py` at `sorry=0 admit=0 axiom=0 native_decide=0`; the 14 + 11 in-file
 2418: or narrower and none touching `sorryAx`; `FinalCheck.lean` acceptance build is `--- OK: FinalCheck.lean
 4538: `--- OK ---`; `Probe/forbidden_tokens.py` at zero; the `#guard_msgs` guards inside the files; and the
 4648: `--- OK ---`; `Probe/forbidden_tokens.py` at zero; the in-file `#guard_msgs`; the `FinalCheck.lean`
 4732: `--- OK ---`; `Probe/forbidden_tokens.py` at zero; the in-file `#guard_msgs`; the `FinalCheck.lean`
 4803: `.olean`s, `--- OK ---` for each; `Probe/forbidden_tokens.py` at zero; the in-file `#guard_msgs`; the
 4888: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 4990: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5023:   import the statement silently elaborates with `sorryAx` (the guards catch it).
 5066: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5131: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5202: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5285: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5372: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5444: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5514: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5586: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5665: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5738: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5813: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5879: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 5946: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 6012: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 6078: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 6137: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 6210: `--- OK ---` for each, `Probe/forbidden_tokens.py` at zero, the in-file `#guard_msgs`, and the
 6460: `open FLMLattice`) is silently turned into a `sorryAx` term; `#print axioms` then reports
 6461: `[propext, sorryAx, Classical.choice, Quot.sound]` and the ONLY symptom is the `#guard_msgs` mismatch.
 7177: **Discipline note**: the `sorryAx` trap FIRED LIVE once in this batch (a stale proof body silently became
 7178: `sorryAx`, caught only by the `#guard_msgs` diff) --- the campaign's guard+probe discipline is load-bearing.
 7433:   `#print axioms` probe over all 16 public declarations --- all clean, no `sorryAx` (recorded here so the
 7476: `sorryAx`).
 7763:   from the agent's own late write); after the final write all three build clean (3x OK, 0 error, 0 sorryAx).
 8223: * verification: tools/build.ps1 OK; forbidden_tokens all zeros; FinalCheck.lean green; every public
 8270: * verification: tools/build.ps1 OK; forbidden_tokens all zeros; FinalCheck.lean green; every public
 8312: * verification: tools/build.ps1 OK; forbidden_tokens all zeros; FinalCheck.lean green; every public
 8352: * verification: tools/build.ps1 OK; forbidden_tokens all zeros; the blacklist audit (b222a_audit.py)
 8379: Every declaration is guarded; its guard prints `[propext, sorryAx, Classical.choice, Quot.sound]`,
 8402: `Probe/forbidden_tokens.py` reads `sorry=1` for exactly these two files --- the registered holes of
 8403: `README.md`'s `sorry` map --- and all zeros elsewhere.  One ledger name was corrected on the way:
=== NOTES.md
  197:     [propext, sorryAx, Classical.choice, Quot.sound]
  199: **`Probe/forbidden_tokens.py` reports `sorry=0` on that file and is right to**: there is no `sorry`
  200: token anywhere in the text.  The `sorryAx` enters through the failed elaboration.  So the two checks
  489: `Probe/forbidden_tokens.py` at `sorry=0 admit=0 axiom=0 native_decide=0`, and every in-file
 1063:   elaborates with `sorryAx` (the guards catch it).
 2077: ### 95.3 The `sorryAx`-from-elaboration-error trap (campaign-level)
 2079: The dispatcher's capstone first reported `[propext, sorryAx, Classical.choice, Quot.sound]` for all three of
 2081: failed to elaborate and Lean replaced them by `sorryAx` terms — with the `#guard_msgs` mismatch as the ONLY
 2690: that catches silent `sorryAx`.  Every future "prove X" on this front must start with the check, and every target
 3389: * Guards: the sorry-consuming declarations print `[propext, sorryAx, Classical.choice, Quot.sound]`;
 3390:   `README.md`'s `sorry` map gained a two-row table for them; `Probe/forbidden_tokens.py` reads
=== FLM-CH8-MAP.md
  145: `python3 Probe/forbidden_tokens.py` reports `sorry=0  admit=0  axiom=0  native_decide=0` over all
  611:   Verified by `python3 Probe/forbidden_tokens.py` over the 44 files matched by
  613:   `sorry=0 admit=0 axiom=0 native_decide=0` — and over both vendored trees (38 files), same result.
  656: * Repository status: greps and `Probe/forbidden_tokens.py` over `Definitions/` (131 `.lean` files,
=== Challenge.lean
=== FinalCheck.lean
 1547: -- It depends on `sorryAx` only through its hypothesis `MM.MoonshineModule.MoonshineConjectureStatement`.
