chore(assurance): tighten budget to real comment-aware counts (SORRY/ADMIT/AXIOM = 0/0/0)

.assurance/budget.txt

@@ -3,18 +3,16 @@
 # Goal: decrease, never raise. Current surface (2026-06), after deleting the
 # circular/vacuous strict-atom proofs.
 #
-# HONEST ACCOUNTING of these counts: the proof tree contains NO live
+# HONEST ACCOUNTING: the proof tree contains NO live `sorry`/`admit` tactic and
-# `sorry`/`admit` tactic and NO theorem/lemma/axiom at all — the three
+# NO theorem/lemma/axiom — the remaining .ec/.lean files are 0-content scaffolds.
-# remaining .ec/.lean files are 0-content scaffolds (verified: grep for
+# axiom-budget.sh is now COMMENT-AWARE (it strips (* *) / -- / /- -/ before
-# theorem|lemma|axiom|sorry|admit|def over proofs/ returns zero matches).
+# counting), so the word "admit"/"sorry" inside the scaffold BANNERS that
-# axiom-budget.sh counts the WORDS "sorry"/"admit" wherever they appear in
+# *describe the deleted cheats* ("whose proof body was `sorry`", "by `admit`")
-# .ec/.lean files, and they appear here only inside the scaffold BANNERS that
+# no longer counts. The real machine count is SORRY=0 ADMIT=0 AXIOM=0; the
-# *describe the deleted cheats* (e.g. "whose proof body was `sorry`", "by
+# 8 banner mentions surface as a prose [warn] only. The budget is the truth (0),
-# `admit`"). So SORRY=4/ADMIT=4 is prose-in-banners, not unproven assertions.
+# so any genuinely NEW live sorry/admit/axiom trips the gate immediately.
-# The budget is held at the current banner word-count so any genuinely NEW
+# The headline threshold claim is honestly "research-only", not "proven".
-# live sorry/admit (which would also add theorem/lemma machinery) trips the
+SORRY=0
-# gate. The headline threshold claim is honestly "research-only", not "proven".
+ADMIT=0
-SORRY=4
-ADMIT=4
 AXIOM=0
 VACUOUS=0

proofs/easycrypt/Magnetar_N1_StrictAtom.eco

@@ -0,0 +1,23 @@
+{
+  "version": 4,
+  "echash": "r2026.05-16-g76bf9e9",
+  "root": { "kind": "ec", "digest": "39b4713e553436b188370f9ba116ab50" },
+  "trace": null,
+  "depends": {
+    "Logic": {
+      "direct": true,
+      "kind": "ec",
+      "digest": "6b500cdc50293d9b0674166fdcc73d7e"
+    },
+    "Pervasive": {
+      "direct": true,
+      "kind": "ec",
+      "digest": "6547baf21b77e623ccd2078cc1a92306"
+    },
+    "Tactics": {
+      "direct": true,
+      "kind": "ec",
+      "digest": "86b1b5cd82f32d0405a70279cdc8b67b"
+    }
+  }
+}

proofs/easycrypt/Magnetar_N5_PVSS_DKG.eco

@@ -0,0 +1,23 @@
+{
+  "version": 4,
+  "echash": "r2026.05-16-g76bf9e9",
+  "root": { "kind": "ec", "digest": "7cc232f55dd97e26c5e3b81f6962679c" },
+  "trace": null,
+  "depends": {
+    "Logic": {
+      "direct": true,
+      "kind": "ec",
+      "digest": "6b500cdc50293d9b0674166fdcc73d7e"
+    },
+    "Pervasive": {
+      "direct": true,
+      "kind": "ec",
+      "digest": "6547baf21b77e623ccd2078cc1a92306"
+    },
+    "Tactics": {
+      "direct": true,
+      "kind": "ec",
+      "digest": "86b1b5cd82f32d0405a70279cdc8b67b"
+    }
+  }
+}