audit(trg): record M2 close delta + reconfirm X headline

Appends a 2026-04-18 (late afternoon) delta section to the TRG audit:

- Suite moved 30/35 → 31/35 via M2 Lagrange closure (commit cc7c693).
- v1.0 baseline moved 8/15 → 9/15.
- Four v1.0 entries remain in-progress: E1, S3, S4, E5.
- E1 Coquelicot-tractable but single-multi-day sprint (not
  session-scoped); coq-coquelicot 3.4.4 now installed on the
  dev machine.
- S3 / S4 / E5 need scope decisions (research-grade otherwise).
- Three cross-cutting blockers unchanged (Parser-fuzz billing,
  17 RSR workflows billing, flake.nix Nix-install).

Headline grade **TRG-X** unchanged. Three of four remaining gaps
are human-owned; the fourth (E1) is an AI-workable multi-day port.

Updated next-re-audit trigger: E1 closure / S3-S4-E5 scope decision
/ billing resolution.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

audits/audit-trg-2026-04-18.md

@@ -247,3 +247,79 @@ This audit's companion classifier registers:
 entries close to passing, or (b) the GitHub Actions billing blocker
 is resolved and evidence collection begins for the parser-fuzz
 ≥24h gate.
+
+---
+
+## Addendum — 2026-04-18 (late afternoon) — delta re-audit
+
+**Trigger met**: canonical-proof-suite moved +1 passing since the
+snapshot above.
+
+### What moved
+
+**Canonical Proof Suite**: 30/35 → **31/35 passing** (v1.1-proposed
+manifest; 8/15 → **9/15** at v1.0 baseline).
+
+- **M2 Lagrange's theorem** — CLOSED, commit `cc7c693`. Prover
+  switch idris2 → rocq. Layer B via `mathcomp.fingroup.cardSg`;
+  headline `lagrangeTheorem (G H : {group gT}) : H \subset G ->
+  #|H| %| #|G|` discharged by `exact: cardSg. Qed.`. Module header
+  carries honest-progress note (library lift, not from-first-
+  principles in this file); Idris2 companion at `M2-lagrange.idr`
+  retained as partial ground-up scaffold.
+
+### What did not move
+
+Four v1.0 entries remain in-progress; none tractable this session
+under the §3.1 Scaffold-Intent rule ("closure requires importing or
+building the missing analytic layer, not renaming hypotheses"):
+
+- **E1 Lyapunov** — `coq-coquelicot` installed in this session
+  (`3.4.4`). Faithful closure is a single multi-day sprint
+  (~800-1500 LOC on top of Coquelicot.Hierarchy + ODE) per
+  AI-WORK-007.md §3.2. A 1D scalar V̇ ≤ 0 inequality was trialled
+  and rejected — the §3.1 rule forbids closing the headline under
+  a weaker statement of the same name for v1.0 entries.
+- **S3 Boltzmann H-theorem**, **S4 Heisenberg uncertainty** — no
+  opam-packaged analytic layer exists for either. Both require
+  multi-week original formalisation or explicit scope re-decisions
+  (Tier 1 alternatives: monotonicity of Shannon entropy under
+  doubly stochastic maps for S3; variance-product bound on
+  discrete random variables for S4). No decision has been made;
+  owner action tracked in AI-WORK-007.md §3.2.
+- **E5 Needham-Schroeder fixed protocol** — Larry Paulson's
+  canonical proof is Isabelle; the Rocq port is not turn-key.
+  Same scope-decision gate as S3/S4.
+
+### Cross-cutting blockers unchanged
+
+- **Parser-fuzz ≥24h clean-run evidence** — strictly blocked on
+  GitHub Actions billing on `hyperpolymath` (YOUR-ACTIONS-todo.md
+  §1). No change since the main audit body.
+- **17 RSR workflows green** — same billing gate.
+- **flake.nix SupplyChain finding** — strictly blocked on Nix
+  install on the dev machine (YOUR-ACTIONS-todo.md §1b). No
+  change since the main audit body.
+
+### Headline grade
+
+**TRG-X** unchanged. The M2 close is a one-entry move on a
+seven-gap chain; three of the remaining four gaps need
+human-owned actions (billing, Nix install, scope decisions for
+S3/S4/E5) and one (E1) needs a multi-day Coquelicot port.
+
+### Updated roadmap
+
+Items 1, 3, 4, 6 from the main roadmap remain the decisive levers.
+Item 1 is now at 31/35; closing requires:
+- E1 Coquelicot port — AI-workable multi-day sprint.
+- S3 / S4 / E5 — scope decision (owner) then multi-week or
+  re-scoped closure (AI).
+
+Items 3 + 4 stay blocked on billing; item 5 substrate remains in
+place (docs-only refactor pending); item 6 M3 reference-oracle
+differential-harness closure is unchanged single-session work.
+
+*Next re-audit trigger*: first of (a) E1 Coquelicot closure, (b) a
+scope decision on S3/S4/E5, or (c) GitHub Actions billing
+resolution.