Expose formula integrity in the Brain HUD

static/3d/brain.html

@@ -66,6 +66,11 @@
  #hud .row .dot{width:9px;height:9px;border-radius:50%;box-shadow:0 0 7px currentColor;flex:0 0 auto}
  #hud .row .right{display:flex;align-items:center;gap:6px}
  #hud .row .val{color:#eef3f6}
+ #hud .attestation{display:block;color:#9fb1bf;font-size:9.5px;line-height:1.45;padding:5px 7px;
+  margin:-2px 0 1px 16px;border-left:2px solid #375464;background:rgba(8,20,15,.58);
+  overflow-wrap:anywhere;word-break:break-word}
+ #hud .attestation[data-state="VERIFIED"]{color:var(--proof);border-left-color:var(--proof)}
+ #hud .attestation[data-state="UNAVAILABLE"]{color:#e08a8a;border-left-color:#e08a8a}
  #hud .note{color:#6d7d8a;font-size:10.5px;line-height:1.45;margin-top:2px;border-top:1px solid #15212c;padding-top:6px}
  #hud .plainbtn{font:11px ui-monospace,monospace;padding:5px 11px;border-radius:7px;border:1px solid var(--proof);
   background:#08140f;color:var(--proof);cursor:pointer;width:fit-content;margin-top:2px}
@@ -199,8 +204,15 @@ const LOBES = [
     dir: [0, 0.55, 0.95], url: "https://github.com/" + GH_ORG + "/a11oy/blob/22b084d4a74abb4d5911ca9dc303c35d222bd284/proofs/lutar-lean/Lutar/Puriq/Formulas/ProvedFormulas.lean",
     fetchStat: async () => {
       const s = requireLive(await EVIDENCE, "formulas");
+      if (s.integrity_state !== "VERIFIED" || s.mutable_reference !== false ||
+          !/^[0-9a-f]{40}$/.test(s.source_commit || "") ||
+          !/^[0-9a-f]{64}$/.test(s.content_sha256 || "")) {
+        throw new Error("formula integrity contract incomplete");
+      }
       const n = s.theorem_count;
       return { text: n + " theorems", honesty: "MEASURED",
+        attestation: "proof artifact · immutable commit " + s.source_commit +
+          " · SHA-256 " + s.content_sha256 + " · " + s.integrity_state,
         caption: "Frontal lobe · " + n + " `theorem` declarations counted server-side from a commit-pinned " +
           "ProvedFormulas.lean artifact · SHA-256 " + s.content_sha256.slice(0, 12) + "… VERIFIED · " +
           "MEASURED via same-origin bounded evidence route · click to read the pinned proofs" };
@@ -560,7 +572,23 @@ function buildHud() {
     hud[key] = { val, chip };
   };
 
-  LOBES.forEach((l) => mkRow(l.key, l.name, l.color));
+  LOBES.forEach((l) => {
+    mkRow(l.key, l.name, l.color);
+    if (l.key === "formulas") {
+      const proof = document.createElement("a");
+      proof.id = "formula-attestation";
+      proof.className = "attestation";
+      proof.href = l.url;
+      proof.target = "_blank";
+      proof.rel = "noopener";
+      proof.setAttribute("aria-live", "polite");
+      proof.dataset.state = "PENDING";
+      proof.textContent = "proof artifact · integrity verification pending…";
+      proof.title = "Open the immutable formula source artifact";
+      hudEl.appendChild(proof);
+      hud[l.key].attestation = proof;
+    }
+  });
 
   const note = document.createElement("div");
   note.className = "note";
@@ -601,6 +629,14 @@ function setRow(key, text, honesty) {
   label.updateChip(r.chip, honesty);
 }
 
+function setFormulaAttestation(text, state) {
+  const proof = hud.formulas && hud.formulas.attestation;
+  if (!proof) return;
+  proof.textContent = text;
+  proof.dataset.state = state;
+  proof.title = text;
+}
+
 // ---------------------------------------------------------------------------
 // pointer picking — hover to caption a lobe, click to open its live source.
 // (Only in orbit mode; mold mode owns the pointer.)
@@ -664,6 +700,7 @@ async function main() {
     try {
       const s = await lobe.fetchStat();
       setRow(lobe.key, s.text, s.honesty);
+      if (lobe.key === "formulas") setFormulaAttestation(s.attestation, "VERIFIED");
       refreshLobeLabel(lobe.key, s.honesty, lobe.name + " \u00b7 " + s.text);
       const lm = lobeMarkers[lobe.key];
       if (lm) lm.marker.userData.caption = s.caption;
@@ -672,6 +709,9 @@ async function main() {
     } catch (e) {
       console.warn("[brain] " + lobe.key + " unavailable:", e && e.message);
       setRow(lobe.key, "NO-LIVE-DATA", "STRUCTURAL-ONLY");
+      if (lobe.key === "formulas") {
+        setFormulaAttestation("proof artifact · integrity UNAVAILABLE · no theorem count trusted", "UNAVAILABLE");
+      }
       refreshLobeLabel(lobe.key, "STRUCTURAL-ONLY", lobe.name + " \u00b7 NO-LIVE-DATA");
       const lm = lobeMarkers[lobe.key];
       if (lm) lm.marker.userData.caption = lobe.name + " \u00b7 NO-LIVE-DATA \u2014 this feed is unreachable right now; nothing is guessed in its place.";

test/test_holographic_zero_cdn.py

@@ -84,6 +84,16 @@ class HolographicZeroCdnTests(unittest.TestCase):
         self.assertEqual(len(holographic._BRAIN_FORMULA_COMMIT), 40)
         self.assertEqual(len(holographic._BRAIN_FORMULA_SHA256), 64)
 
+    def test_formula_integrity_is_persistently_visible_not_hover_only(self):
+        brain = (Path(__file__).parents[1] / "static" / "3d" / "brain.html").read_text(encoding="utf-8")
+        self.assertIn('proof.id = "formula-attestation"', brain)
+        self.assertIn('proof.setAttribute("aria-live", "polite")', brain)
+        self.assertIn('s.source_commit', brain)
+        self.assertIn('s.content_sha256', brain)
+        self.assertIn('s.integrity_state', brain)
+        self.assertIn('setFormulaAttestation(s.attestation, "VERIFIED")', brain)
+        self.assertIn('integrity UNAVAILABLE · no theorem count trusted', brain)
+
     def test_formula_hash_mismatch_is_unavailable_not_measured(self):
         payload = holographic.brain_evidence(
             fetch_json=self._json,