docs(honesty): clarify sorry/admit budget provenance + fix stale THBS-SPEC framing

- .assurance/budget.txt: the SORRY=4/ADMIT=4 counts are axiom-budget.sh
  counting the WORDS 'sorry'/'admit' inside the scaffold BANNERS that
  describe the DELETED cheats, not live tactics. The proof tree has zero
  theorem/lemma/axiom/sorry/admit (verified). Document this so the budget
  is not misread as 8 unproven assertions.
- THBS-SPEC.md: the v1.0 framing said Combine routes via
  circl/slhdsa.SignDeterministic directly; the live code uses the internal
  slhSignAtom engine (byte-identical to circl on the reconstructed master).
  Point to ASSEMBLE-INVARIANT.md as authoritative; reaffirm RESEARCH-ONLY.

No code or proof-state change; M-family claims unchanged (all CONFIRMED).

.assurance/budget.txt

@@ -1,9 +1,19 @@
 # Unproven-assertion budget (max counts). Enforced by
 # ~/work/lux/luxfi/security/framework/checks/axiom-budget.sh. FAILS on any drift above.
 # Goal: decrease, never raise. Current surface (2026-06), after deleting the
-# circular/vacuous strict-atom proofs. The remaining 4 sorry + 4 admit are in
-# SUPPORTING (non-load-bearing) lemmas, disclosed in PROOF-CLAIMS; the headline
-# threshold claim is now honestly "research-only", not "proven".
+# circular/vacuous strict-atom proofs.
+#
+# HONEST ACCOUNTING of these counts: the proof tree contains NO live
+# `sorry`/`admit` tactic and NO theorem/lemma/axiom at all — the three
+# remaining .ec/.lean files are 0-content scaffolds (verified: grep for
+# theorem|lemma|axiom|sorry|admit|def over proofs/ returns zero matches).
+# axiom-budget.sh counts the WORDS "sorry"/"admit" wherever they appear in
+# .ec/.lean files, and they appear here only inside the scaffold BANNERS that
+# *describe the deleted cheats* (e.g. "whose proof body was `sorry`", "by
+# `admit`"). So SORRY=4/ADMIT=4 is prose-in-banners, not unproven assertions.
+# The budget is held at the current banner word-count so any genuinely NEW
+# live sorry/admit (which would also add theorem/lemma machinery) trips the
+# gate. The headline threshold claim is honestly "research-only", not "proven".
 SORRY=4
 ADMIT=4
 AXIOM=0

THBS-SPEC.md

@@ -46,12 +46,18 @@ EVER reconstructs SK.seed, even transiently in memory" --- requires
 the v1.1 strict-atom-assembly path tracked at
 `BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11`.
 
-Magnetar v1.0 routes the final FIPS 205 byte production via
-`circl/slhdsa.SignDeterministic` on a seed reconstructed by the
-PUBLIC COMBINER. The seed is briefly present in the public combiner's
-memory for one Sign call and is zeroized before return. The combiner
-role is PUBLIC --- anyone can be the combiner --- and there is no
-long-lived secret material outside party-local Shamir leaves.
+Magnetar v1.0 routes the final FIPS 205 byte production via the
+Magnetar-internal `slhSignAtom` engine (`thbsse_assemble.go`) on a
+master reconstructed by the PUBLIC COMBINER; the emitted bytes are
+byte-identical to `circl/slhdsa.SignDeterministic` on that same master
+(pinned by `TestSlhdsaInternal_ByteEqualToCirclSign` and
+`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`). The master is
+briefly present in the public combiner's memory for one Sign call and
+is zeroized before return. The combiner role is PUBLIC --- anyone can
+be the combiner --- and there is no long-lived secret material outside
+party-local Shamir leaves. (The authoritative current description of
+this path is `ASSEMBLE-INVARIANT.md`; this is the RESEARCH-ONLY leg,
+not production --- see §1.0 of `SPEC.md`.)
 
 This is materially stronger than a TEE-attested privileged-aggregator
 model (no host is in the TCB) and materially weaker than the strict