Spaces:

SZLHOLDINGS
/

a11oy

Running

File size: 68,447 Bytes

<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>a11oy — Verifiable Inference</title>
<style>
  /* =====================================================================
     a11oy Tier-1 Demo — elite showcase aesthetic
     Dark palette · Cabinet Grotesk / JetBrains Mono · honest-label chips
     ===================================================================== */
  @import url('https://fonts.googleapis.com/css2?family=JetBrains+Mono:ital,wght@0,400;0,600;1,400&display=swap');

  :root {
    --bg:        #0a0c0f;
    --bg-panel:  #111318;
    --bg-card:   #16191f;
    --border:    #2a2d35;
    --border-hi: #3d4250;
    --text:      #e8eaf0;
    --text-dim:  #8891a8;
    --text-mute: #4a5068;
    --accent:    #6c8ef5;
    --accent-hi: #8aaaf8;
    --green:     #4ade80;
    --amber:     #f59e0b;
    --red:       #f87171;
    --mono:      'JetBrains Mono', 'Fira Code', 'Cascadia Code', monospace;
    --sans:      'Cabinet Grotesk', 'Inter', 'Segoe UI', system-ui, sans-serif;
    --radius:    8px;
    --radius-lg: 14px;
    --shadow:    0 2px 12px rgba(0,0,0,0.5);
  }

  *, *::before, *::after { box-sizing: border-box; margin: 0; padding: 0; }

  body {
    background: var(--bg);
    color: var(--text);
    font-family: var(--sans);
    font-size: 15px;
    line-height: 1.6;
    min-height: 100vh;
  }

  /* ---- header ---- */
  .site-header {
    border-bottom: 1px solid var(--border);
    padding: 18px 32px;
    display: flex;
    align-items: center;
    gap: 16px;
    background: var(--bg-panel);
  }
  .logo-mark {
    width: 32px; height: 32px;
    flex-shrink: 0;
  }
  .site-title { font-size: 16px; font-weight: 700; letter-spacing: -0.02em; }
  .site-tagline { font-size: 12px; color: var(--text-dim); margin-left: auto; }
  .nav-back {
    font-size: 12px; color: var(--text-dim);
    text-decoration: none; margin-left: auto;
    border: 1px solid var(--border); border-radius: 6px;
    padding: 5px 12px;
    transition: border-color .15s, color .15s;
  }
  .nav-back:hover { border-color: var(--accent); color: var(--accent-hi); }

  /* ---- layout ---- */
  .page { max-width: 900px; margin: 0 auto; padding: 48px 24px 80px; }
  .page-hero { margin-bottom: 56px; }
  .page-hero h1 {
    font-size: 28px; font-weight: 800; letter-spacing: -0.03em;
    line-height: 1.2; margin-bottom: 10px;
  }
  .page-hero p { color: var(--text-dim); max-width: 600px; }

  /* ---- sections ---- */
  .section {
    margin-bottom: 56px;
    border: 1px solid var(--border);
    border-radius: var(--radius-lg);
    overflow: hidden;
  }
  .section-head {
    background: var(--bg-panel);
    padding: 20px 24px;
    border-bottom: 1px solid var(--border);
  }
  .section-head h2 {
    font-size: 16px; font-weight: 700; letter-spacing: -0.01em;
    margin-bottom: 4px; display: flex; align-items: center; gap: 10px;
  }
  .section-label {
    font-size: 10px; font-weight: 700; letter-spacing: 0.08em;
    text-transform: uppercase; color: var(--text-dim);
    border: 1px solid var(--border-hi); border-radius: 4px;
    padding: 2px 6px;
  }
  .section-head p { font-size: 13px; color: var(--text-dim); max-width: 620px; }
  .section-body { padding: 24px; background: var(--bg-card); }
  .moat-line {
    font-size: 12px; color: var(--text-dim);
    font-style: italic; margin-top: 8px;
  }

  /* ---- chip / badges ---- */
  .chip {
    display: inline-block; border-radius: 4px;
    padding: 2px 8px; font-size: 11px; font-weight: 700;
    letter-spacing: 0.05em; text-transform: uppercase;
    border: 1px solid transparent;
  }
  .chip-allow  { background: #052e12; border-color: #166534; color: var(--green); }
  .chip-review { background: #2d1e00; border-color: #92400e; color: var(--amber); }
  .chip-deny   { background: #2d0f0f; border-color: #991b1b; color: var(--red); }
  .chip-info   { background: #0d1533; border-color: #1e3a8a; color: var(--accent-hi); }
  .chip-dim    { background: #1a1d24; border-color: var(--border); color: var(--text-dim); }
  .chip-ok     { background: #052e12; border-color: #166534; color: var(--green); }
  .chip-warn   { background: #2d1e00; border-color: #92400e; color: var(--amber); }
  .chip-err    { background: #2d0f0f; border-color: #991b1b; color: var(--red); }

  /* ---- buttons ---- */
  .btn-row { display: flex; gap: 10px; flex-wrap: wrap; margin-bottom: 20px; }
  .btn {
    padding: 9px 18px; border-radius: var(--radius);
    font-family: var(--sans); font-size: 13px; font-weight: 600;
    cursor: pointer; border: 1px solid transparent;
    transition: opacity .15s, transform .05s;
    outline: none;
  }
  .btn:active { transform: scale(0.97); }
  .btn-primary {
    background: #1e3a8a; border-color: #2563eb;
    color: #dbeafe;
  }
  .btn-primary:hover { background: #1d4ed8; }
  .btn-allow  { background: #052e12; border-color: #166534; color: var(--green); }
  .btn-allow:hover  { background: #14532d; }
  .btn-review { background: #2d1e00; border-color: #92400e; color: var(--amber); }
  .btn-review:hover { background: #451a03; }
  .btn-deny   { background: #2d0f0f; border-color: #991b1b; color: var(--red); }
  .btn-deny:hover   { background: #450a0a; }
  .btn:disabled { opacity: 0.5; cursor: not-allowed; }

  /* ---- output panels ---- */
  .output {
    background: var(--bg-panel); border: 1px solid var(--border);
    border-radius: var(--radius); padding: 16px 20px;
    font-family: var(--mono); font-size: 12px; line-height: 1.7;
    white-space: pre-wrap; word-break: break-all;
    color: var(--text-dim); min-height: 56px;
    transition: border-color .2s;
  }
  .output.verified   { border-color: #166534; }
  .output.failed     { border-color: #991b1b; }
  .output.loading    { border-color: var(--accent); animation: pulse 1s ease-in-out infinite; }
  @keyframes pulse { 0%,100%{opacity:.8} 50%{opacity:.4} }

  /* ---- verdict banner ---- */
  .verdict-banner {
    border-radius: var(--radius); padding: 14px 20px;
    margin-bottom: 16px; font-size: 14px; font-weight: 700;
    display: flex; align-items: center; gap: 12px;
    border: 1px solid transparent;
  }
  .verdict-ok  { background: #052e12; border-color: #166534; color: var(--green); }
  .verdict-fail{ background: #2d0f0f; border-color: #991b1b; color: var(--red); }
  .verdict-dim { background: var(--bg-panel); border-color: var(--border); color: var(--text-dim); }

  /* ---- formula cards ---- */
  .formula-grid { display: grid; gap: 14px; }
  .formula-card {
    background: var(--bg-panel); border: 1px solid var(--border);
    border-radius: var(--radius); padding: 16px 20px;
  }
  .formula-card-head {
    display: flex; align-items: center; gap: 10px; margin-bottom: 8px;
  }
  .formula-id {
    font-family: var(--mono); font-size: 11px; font-weight: 600;
    color: var(--accent); background: #0d1533; border: 1px solid #1e3a8a;
    border-radius: 4px; padding: 2px 7px;
  }
  .formula-name { font-size: 14px; font-weight: 700; }
  .formula-lean {
    font-family: var(--mono); font-size: 12px; color: #a5f3fc;
    background: #051e24; border: 1px solid #0e4a57;
    border-radius: 6px; padding: 10px 14px; margin: 8px 0;
    white-space: pre-wrap; word-break: break-all; line-height: 1.6;
  }
  .formula-desc { font-size: 12px; color: var(--text-dim); }
  .formula-status {
    font-size: 10px; color: var(--green); font-family: var(--mono);
    margin-top: 6px;
  }

  /* ---- corpus diagram ---- */
  .corpus-diagram {
    display: flex; gap: 14px; flex-wrap: wrap; margin: 20px 0;
  }
  .corpus-tier {
    flex: 1; min-width: 180px;
    border: 1px solid var(--border); border-radius: var(--radius);
    padding: 16px; background: var(--bg-panel);
  }
  .corpus-count {
    font-size: 32px; font-weight: 800; font-family: var(--mono);
    line-height: 1;
  }
  .corpus-count.proven { color: var(--green); }
  .corpus-count.gates  { color: var(--amber); }
  .corpus-count.total  { color: var(--accent-hi); }
  .corpus-tier-label { font-size: 11px; font-weight: 700; text-transform: uppercase;
    letter-spacing: 0.07em; margin: 4px 0 8px; }
  .corpus-tier-desc { font-size: 12px; color: var(--text-dim); }
  .corpus-never-claim {
    background: #2d1e00; border: 1px solid #92400e;
    border-radius: var(--radius); padding: 12px 16px;
    font-size: 13px; color: var(--amber); margin-top: 14px;
  }

  /* ---- hash display ---- */
  .hash-row {
    display: flex; gap: 8px; align-items: center;
    flex-wrap: wrap; margin: 6px 0;
  }
  .hash-label { font-size: 11px; color: var(--text-dim); min-width: 90px; }
  .hash-val {
    font-family: var(--mono); font-size: 11px; color: var(--text);
    background: var(--bg); border-radius: 4px; padding: 2px 6px;
    border: 1px solid var(--border); word-break: break-all;
  }
  .hash-match { border-color: #166534; color: var(--green); }
  .hash-mismatch { border-color: #991b1b; color: var(--red); }

  /* ---- gate row ---- */
  .gate-row {
    display: flex; align-items: center; gap: 12px;
    padding: 8px 12px; border-radius: 6px;
    background: var(--bg); border: 1px solid var(--border);
    margin-bottom: 6px;
  }
  .gate-name { font-family: var(--mono); font-size: 12px; flex: 1; }
  .gate-fired { font-size: 11px; font-weight: 700; }

  /* ---- loading spinner ---- */
  .spinner {
    display: inline-block; width: 14px; height: 14px;
    border: 2px solid var(--border); border-top-color: var(--accent);
    border-radius: 50%; animation: spin .7s linear infinite;
    vertical-align: middle; margin-right: 6px;
  }
  @keyframes spin { to { transform: rotate(360deg); } }

  /* ---- status line ---- */
  .status-line { font-size: 12px; color: var(--text-dim); margin-top: 8px; }

  /* ---- divider ---- */
  .divider { border: none; border-top: 1px solid var(--border); margin: 20px 0; }

  /* ---- conjecture chip ---- */
  .conj {
    display: inline-block;
    font-size: 10px; font-weight: 700; letter-spacing: 0.06em;
    text-transform: uppercase; border-radius: 4px;
    padding: 2px 7px; border: 1px solid #92400e;
    background: #2d1e00; color: var(--amber);
  }

  /* ---- footer ---- */
  .footer {
    border-top: 1px solid var(--border); padding: 24px;
    color: var(--text-mute); font-size: 12px; text-align: center;
  }
  a { color: var(--accent); text-decoration: none; }
  a:hover { color: var(--accent-hi); text-decoration: underline; }
</style>
</head>
<body>

<!-- ===== HEADER ===== -->
<header class="site-header">
  <svg class="logo-mark" viewBox="0 0 32 32" fill="none" aria-label="a11oy">
    <rect width="32" height="32" rx="7" fill="#1e3a8a"/>
    <path d="M8 24 L16 8 L24 24" stroke="#6c8ef5" stroke-width="2.5" stroke-linecap="round" stroke-linejoin="round" fill="none"/>
    <circle cx="16" cy="16" r="2.5" fill="#8aaaf8"/>
  </svg>
  <span class="site-title">a11oy</span>
  <span class="site-tagline">Governed Inference · Verifiable by Design</span>
  <a href="/" class="nav-back">← Console</a>
</header>

<!-- ===== MAIN ===== -->
<main class="page">

  <div class="page-hero">
    <h1>Verifiable Inference</h1>
    <p>Real, verifiable governance receipts — including our own public ledger. Every receipt is signed and independently verifiable. The honesty is the product.</p>
  </div>

  <!-- ===================================================================
       SECTION A — Buyer-Verifiable Receipt (BVIR)
       =================================================================== -->
  <section class="section" id="section-bvir">
    <div class="section-head">
      <h2>
        <span class="section-label">A</span>
        Buyer-Verifiable Inference Receipt
      </h2>
      <p>
        Makes a real POST /api/a11oy/v1/govern/infer call, then verifies the DSSE ECDSA-P256
        signature <strong>in-browser</strong> using WebCrypto — no server round-trip for verification.
        SHA-256 of the decoded payload is recomputed and matched to <code>receipt.payload_digest</code>.
      </p>
      <p class="moat-line">
        "No other inference provider gives you a receipt you can re-verify yourself, offline, with just a hash function and our public key."
      </p>
    </div>
    <div class="section-body">

      <div class="btn-row">
        <button class="btn btn-primary" id="bvir-run" onclick="runBVIR()">
          Run Inference &amp; Verify Receipt
        </button>
      </div>

      <div id="bvir-status" class="status-line"></div>
      <div id="bvir-verdict" style="display:none"></div>
      <div id="bvir-output" class="output" style="display:none"></div>

    </div>
  </section>

  <!-- ===================================================================
       SECTION B — Λ-Gated Honest Refusal
       =================================================================== -->
  <section class="section" id="section-govern">
    <div class="section-head">
      <h2>
        <span class="section-label">B</span>
        Λ-Gated Honest Refusal
      </h2>
      <p>
        Three preset governance cases. Each returns a REAL signed receipt via
        <code>szl_dsse.sign_khipu_receipt</code>. Λ is always labeled
        <span class="conj">Conjecture 1 — advisory, NOT a theorem</span>.
      </p>
      <p class="moat-line">"Even our refusals are signed and explained — no black-box boolean."</p>
    </div>
    <div class="section-body">

      <div class="btn-row">
        <button class="btn btn-allow"  onclick="runGovern('allow')">Allow</button>
        <button class="btn btn-review" onclick="runGovern('review')">Review</button>
        <button class="btn btn-deny"   onclick="runGovern('deny')">Deny</button>
      </div>

      <div id="govern-status" class="status-line"></div>
      <div id="govern-panel" style="display:none">
        <div id="govern-verdict-banner"></div>
        <div id="govern-lambda-row" style="margin-bottom:14px"></div>
        <div id="govern-gates"></div>
        <div id="govern-receipt-block" style="display:none;margin-top:16px">
          <div style="font-size:12px;font-weight:700;color:var(--text-dim);margin-bottom:8px;text-transform:uppercase;letter-spacing:.06em">Signed Denial Receipt</div>
          <div id="govern-receipt-output" class="output"></div>
        </div>
      </div>

    </div>
  </section>

  <!-- ===================================================================
       SECTION C — Verifiable Thesis
       =================================================================== -->
  <section class="section" id="section-thesis">
    <div class="section-head">
      <h2>
        <span class="section-label">C</span>
        Verifiable Thesis
      </h2>
      <p>
        The 8 PROVEN formulas with verbatim Lean 4 statements, the 3-tier honest corpus
        (8 / ~35 / ~185), and the honest conjecture labels for Λ and Khipu BFT.
      </p>
      <p class="moat-line">"The honesty is the product. Click any formula — verify it yourself."</p>
    </div>
    <div class="section-body">

      <div class="btn-row">
        <button class="btn btn-primary" id="thesis-load" onclick="loadThesis()">
          Load Formulas &amp; Corpus
        </button>
      </div>

      <div id="thesis-status" class="status-line"></div>
      <div id="thesis-panel" style="display:none">

        <!-- corpus diagram -->
        <div id="thesis-corpus"></div>

        <hr class="divider" />

        <!-- 8 formulas -->
        <div style="font-size:13px;font-weight:700;margin-bottom:14px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em">
          8 Kernel-Proven Formulas
        </div>
        <div id="thesis-formulas" class="formula-grid"></div>

        <hr class="divider" />

        <!-- conjecture labels -->
        <div id="thesis-conjectures"></div>

      </div>

    </div>
  </section>

  <!-- ===================================================================
       SECTION D — Public Ledger (real receipts from szl-lake)
       =================================================================== -->
  <section class="section" id="section-ledger">
    <div class="section-head">
      <h2>
        <span class="section-label">D</span>
        Public Ledger — Real Receipts
      </h2>
      <p>
        Real signed Khipu receipts from our public dataset
        <a href="https://huggingface.co/datasets/SZLHOLDINGS/szl-lake" target="_blank" rel="noopener">SZLHOLDINGS/szl-lake</a>
        (snapshot 2026-07-02). This page recomputes the <strong>hash-chain linkage in your browser</strong>;
        the DSSE / sigstore signatures verify <strong>offline</strong> with the
        <a href="https://pypi.org/project/szl-receipt/" target="_blank" rel="noopener">szl-receipt</a>
        library and cross-check against the canonical rows on Hugging Face — infrastructure we do not control.
      </p>
      <p class="moat-line">"The receipts you would read in diligence — including the ones where we mark our own central claim, &Lambda;, still OPEN."</p>
    </div>
    <div class="section-body">
      <div class="btn-row">
        <button class="btn btn-primary" id="ledger-load" onclick="renderLedger()">
          Load Public Ledger &amp; Check Chain
        </button>
      </div>
      <div id="ledger-status" class="status-line"></div>
      <div id="ledger-panel" style="display:none">
        <div id="ledger-chain"></div>
        <hr class="divider" />
        <div id="ledger-cards"></div>
      </div>
    </div>
  </section>

</main>

<footer class="footer">
  <p>SZL Holdings · a11oy · Doctrine v11 · 8 kernel-verified formulas @ c7c0ba17 ·
     Λ = Conjecture 1 (advisory) · Khipu BFT = Conjecture 2 ·
     <a href="/govern/health" target="_blank">Governance Health</a> ·
     <a href="/api/a11oy/v1/demo/thesis" target="_blank">Thesis API</a>
  </p>
</footer>

<!-- ===================================================================
     JAVASCRIPT — all in-browser, no CDN
     =================================================================== -->
<script>
"use strict";

/* ---- utility ---- */
function el(id) { return document.getElementById(id); }
function show(id) { const e = el(id); if (e) e.style.display = ''; }
function hide(id) { const e = el(id); if (e) e.style.display = 'none'; }
function setText(id, txt) { const e = el(id); if (e) e.textContent = txt; }
function setHTML(id, html) { const e = el(id); if (e) e.innerHTML = html; }

function setStatus(id, msg, loading) {
  const e = el(id);
  if (!e) return;
  if (loading) {
    e.innerHTML = '<span class="spinner"></span>' + escHTML(msg);
  } else {
    e.textContent = msg;
  }
}

function escHTML(s) {
  return String(s)
    .replace(/&/g,'&amp;')
    .replace(/</g,'&lt;')
    .replace(/>/g,'&gt;')
    .replace(/"/g,'&quot;');
}

/* ---- base64 helpers ---- */
function b64Decode(s) {
  // standard base64 → Uint8Array (not URL-safe; WebCrypto importKey returns SPKI base64)
  const bin = atob(s);
  const b = new Uint8Array(bin.length);
  for (let i = 0; i < bin.length; i++) b[i] = bin.charCodeAt(i);
  return b;
}

function b64Encode(buf) {
  let s = '';
  const b = new Uint8Array(buf);
  for (let i = 0; i < b.length; i++) s += String.fromCharCode(b[i]);
  return btoa(s);
}

/* ---- DER ASN.1 → raw r‖s converter (for WebCrypto ECDSA P-256) ----
   cosign / cryptography-lib ECDSA signs in DER (ASN.1 SEQUENCE { INTEGER r, INTEGER s }).
   WebCrypto ECDSA P-256 SHA-256 expects IEEE P-1363 raw r‖s (64 bytes: 32+32).
   We decode the DER SEQUENCE here entirely in JS — no library needed.
*/
function derToRaw(derBytes) {
  let i = 0;
  if (derBytes[i++] !== 0x30) throw new Error('not DER SEQUENCE');
  // Length (short form or long form)
  let seqLen = derBytes[i++];
  if (seqLen & 0x80) {
    const nb = seqLen & 0x7f;
    seqLen = 0;
    for (let b = 0; b < nb; b++) seqLen = (seqLen << 8) | derBytes[i++];
  }
  function readInt() {
    if (derBytes[i++] !== 0x02) throw new Error('expected INTEGER tag');
    let len = derBytes[i++];
    if (len & 0x80) {
      const nb = len & 0x7f; len = 0;
      for (let b = 0; b < nb; b++) len = (len << 8) | derBytes[i++];
    }
    const val = derBytes.slice(i, i + len); i += len;
    return val;
  }
  const rArr = readInt();
  const sArr = readInt();
  // Pad / strip prefix zero byte (ASN.1 adds 0x00 prefix when high-bit is set)
  function pad32(arr) {
    // strip prefix 0x00 byte
    let j = 0;
    while (j < arr.length - 1 && arr[j] === 0) j++;
    const stripped = arr.slice(j);
    const out = new Uint8Array(32);
    const off = 32 - stripped.length;
    if (off < 0) throw new Error('integer too long: ' + stripped.length);
    out.set(stripped, off);
    return out;
  }
  const raw = new Uint8Array(64);
  raw.set(pad32(rArr), 0);
  raw.set(pad32(sArr), 32);
  return raw;
}

/* ---- DSSE PAE ----
   PAE(type, body) = "DSSEv1" SP LEN(type) SP type SP LEN(body) SP body
   Exactly mirrors szl_dsse.pae()
*/
function buildPAE(payloadType, bodyBytes) {
  const enc = new TextEncoder();
  const t = enc.encode(payloadType);
  const prefix = enc.encode(`DSSEv1 ${t.length} `);
  const mid = enc.encode(` ${bodyBytes.length} `);
  const total = prefix.length + t.length + mid.length + bodyBytes.length;
  const buf = new Uint8Array(total);
  let off = 0;
  buf.set(prefix, off); off += prefix.length;
  buf.set(t, off); off += t.length;
  buf.set(mid, off); off += mid.length;
  buf.set(bodyBytes, off);
  return buf;
}

/* ---- SHA-256 via WebCrypto ---- */
async function sha256(data) {
  const hash = await crypto.subtle.digest('SHA-256', data);
  return Array.from(new Uint8Array(hash)).map(b => b.toString(16).padStart(2,'0')).join('');
}

/* ---- Import P-256 SPKI public key from PEM ---- */
async function importPubKeyFromPEM(pem) {
  const b64 = pem
    .replace('-----BEGIN PUBLIC KEY-----','')
    .replace('-----END PUBLIC KEY-----','')
    .replace(/\s+/g,'');
  const raw = b64Decode(b64);
  return crypto.subtle.importKey(
    'spki', raw.buffer,
    { name: 'ECDSA', namedCurve: 'P-256' },
    false, ['verify']
  );
}

/* ====================================================================
   SECTION A — BVIR
   ==================================================================== */
async function runBVIR() {
  const btn = el('bvir-run');
  btn.disabled = true;
  hide('bvir-verdict');
  hide('bvir-output');
  setStatus('bvir-status', 'Calling /api/a11oy/v1/govern/infer …', true);

  let data;
  try {
    const resp = await fetch('/api/a11oy/v1/govern/infer', {
      method: 'POST',
      headers: { 'Content-Type': 'application/json' },
      body: JSON.stringify({ prompt: 'hello', vertical: 'general', declared: 'PUBLIC' })
    });
    data = await resp.json();
  } catch(e) {
    setStatus('bvir-status', 'Error calling govern/infer: ' + e.message);
    btn.disabled = false;
    return;
  }

  setStatus('bvir-status', 'Verifying signature in-browser via WebCrypto …', true);

  const dsse   = data.dsse   || {};
  const receipt= data.receipt|| {};

  // A demo-signed receipt is signed by the clearly-labelled demo-signing-key, NOT
  // the production founder-gated cosign key. We must verify it against the DEMO
  // public key (/demo-cosign.pub), and the badge must say so explicitly.
  const dsseKeyid = ((dsse.signatures || [])[0] || {}).keyid || dsse.key_id || '';
  const isDemoKey = dsseKeyid === 'demo-signing-key';
  const pubKeyURL = isDemoKey ? '/demo-cosign.pub' : '/cosign.pub';

  // Step 1: Fetch the matching public key (production cosign.pub, or demo-cosign.pub)
  let pubKey;
  let pubKeyPEM = '';
  try {
    const pkResp = await fetch(pubKeyURL);
    pubKeyPEM = await pkResp.text();
    pubKey = await importPubKeyFromPEM(pubKeyPEM);
  } catch(e) {
    setStatus('bvir-status', 'Could not fetch/import ' + pubKeyURL + ': ' + e.message);
    btn.disabled = false;
    return;
  }

  // Step 2: Decode payload bytes
  const payloadType = dsse.payloadType || 'application/vnd.szl.khipu+json';
  let payloadBytes;
  try {
    payloadBytes = b64Decode(dsse.payload || '');
  } catch(e) {
    setStatus('bvir-status', 'Could not decode dsse.payload: ' + e.message);
    btn.disabled = false;
    return;
  }

  // Step 3: Recompute SHA-256 of decoded payload
  const payloadDigestComputed = await sha256(payloadBytes.buffer);

  // Step 4: PAE and verify signature
  const paeBytes = buildPAE(payloadType, payloadBytes);
  const paeSHA   = await sha256(paeBytes.buffer);

  const sigs = dsse.signatures || [];
  let verified = false;
  let verifyError = '';
  let sigKeyid = '';

  if (!dsse.signed) {
    verifyError = 'UNSIGNED envelope — private key not available in this runtime. Receipt chain is still valid.';
  } else if (sigs.length === 0) {
    verifyError = 'No signatures in envelope.';
  } else {
    const sigEntry = sigs[0];
    sigKeyid = sigEntry.keyid || '';
    try {
      // Try IEEE P-1363 raw first; if that fails, try DER
      const sigBytes = b64Decode(sigEntry.sig || '');
      let rawSig = sigBytes;

      // Detect DER: starts with 0x30
      if (sigBytes[0] === 0x30) {
        try {
          rawSig = derToRaw(sigBytes);
        } catch(e2) {
          verifyError = 'DER→raw conversion failed: ' + e2.message;
        }
      }

      if (!verifyError) {
        verified = await crypto.subtle.verify(
          { name: 'ECDSA', hash: 'SHA-256' },
          pubKey,
          rawSig.buffer,
          paeBytes.buffer
        );
        if (!verified) {
          // Try without DER conversion (in case it was already raw)
          if (sigBytes[0] === 0x30) {
            verified = await crypto.subtle.verify(
              { name: 'ECDSA', hash: 'SHA-256' },
              pubKey,
              sigBytes.buffer,
              paeBytes.buffer
            );
          }
        }
        if (!verified) verifyError = 'ECDSA verification returned false.';
      }
    } catch(e) {
      verifyError = 'Signature verify error: ' + e.message;
    }
  }

  // Step 5: Hash-chain check
  // IMPORTANT: keep the receipt's DECLARED payload digest separate from the
  // chain/receipt id. receipt.digest is the chain id; receipt.payload_digest is
  // the digest the receipt DECLARES for its payload. The MATCH/MISMATCH chip must
  // compare the recomputed payload sha256 against the DECLARED payload digest only,
  // never against the chain id (that comparison is meaningless and would show a
  // spurious red MISMATCH next to a genuinely VERIFIED signature).
  const declaredPayloadDigest = String(receipt.payload_digest || '').toLowerCase();
  const hasDeclaredDigest      = declaredPayloadDigest.length > 0;
  const payloadDigestMatches   = hasDeclaredDigest &&
        (payloadDigestComputed.toLowerCase() === declaredPayloadDigest);
  const chainPrev       = receipt.prev || '(genesis)';
  const chainDigest     = receipt.digest || '';

  // Build result UI
  let verdictHTML = '';
  if (verified && isDemoKey) {
    verdictHTML = `<div class="verdict-banner verdict-ok">
      ✓ VERIFIED (demo-signing-key — not the production cosign key)
      <span class="chip chip-ok">keyid: ${escHTML(sigKeyid)}</span>
      <div style="font-size:12px;font-weight:400;margin-top:6px;color:var(--text-dim)">
        Real ECDSA-P256 signature, verified in your browser against /demo-cosign.pub.
        This is a clearly-labelled DEMO key — the production cosign key stays
        founder-gated and is never placed in this runtime.
      </div>
    </div>`;
  } else if (verified) {
    verdictHTML = `<div class="verdict-banner verdict-ok">
      ✓ VERIFIED — WebCrypto ECDSA-P256 signature valid
      <span class="chip chip-ok">keyid: ${escHTML(sigKeyid)}</span>
    </div>`;
  } else if (!dsse.signed) {
    verdictHTML = `<div class="verdict-banner verdict-dim">
      ⚠ UNSIGNED — private key not in runtime; receipt chain still valid
    </div>`;
  } else {
    verdictHTML = `<div class="verdict-banner verdict-fail">
      ✗ VERIFICATION FAILED — ${escHTML(verifyError)}
    </div>`;
  }

  // Two clearly separate, non-contradictory results:
  //   (1) signature verify   -> shown in the verdict banner above
  //   (2) payload-digest match -> computed sha256 vs the receipt's DECLARED payload_digest
  // When the receipt declares no payload_digest we show an honest neutral state,
  // NEVER a red MISMATCH.
  let digestChipClass, digestChipText, digestValClass;
  if (!hasDeclaredDigest) {
    digestChipClass = 'chip-dim';
    digestChipText  = 'NO DECLARED DIGEST';
    digestValClass  = '';
  } else if (payloadDigestMatches) {
    digestChipClass = 'chip-ok';
    digestChipText  = 'MATCH';
    digestValClass  = 'hash-match';
  } else {
    digestChipClass = 'chip-err';
    digestChipText  = 'MISMATCH';
    digestValClass  = 'hash-mismatch';
  }

  verdictHTML += `
    <div style="margin-bottom:12px">
      <div class="hash-row">
        <span class="hash-label">Signature verify:</span>
        <span class="chip ${verified ? 'chip-ok' : (dsse.signed === false ? 'chip-dim' : 'chip-err')}">${verified ? 'VERIFIED' : (dsse.signed === false ? 'UNSIGNED' : 'FAILED')}</span>
      </div>
      <div class="hash-row">
        <span class="hash-label">Payload digest:</span>
        <span class="hash-val ${digestValClass}">${payloadDigestComputed.substring(0,32)}…</span>
        <span class="chip ${digestChipClass}">${digestChipText}</span>
      </div>
      ${hasDeclaredDigest ? `<div class="hash-row">
        <span class="hash-label">Declared digest:</span>
        <span class="hash-val">${escHTML(declaredPayloadDigest.substring(0,32))}…</span>
      </div>` : `<div class="hash-row">
        <span class="hash-label">Declared digest:</span>
        <span class="hash-val" style="color:var(--text-dim)">(none declared — nothing to compare against)</span>
      </div>`}
      <div class="hash-row">
        <span class="hash-label">PAE SHA-256:</span>
        <span class="hash-val">${paeSHA.substring(0,32)}…</span>
      </div>
      <div class="hash-row">
        <span class="hash-label">Chain prev:</span>
        <span class="hash-val">${escHTML(String(chainPrev).substring(0,32))}…</span>
      </div>
      <div class="hash-row">
        <span class="hash-label">Chain digest:</span>
        <span class="hash-val">${escHTML(String(chainDigest).substring(0,32))}…</span>
      </div>
    </div>
    <div style="font-size:12px;color:var(--text-dim);margin-bottom:8px">
      <span class="conj">Λ Conjecture 1 — advisory</span>
      Λ = ${escHTML(String((data.governance||{}).lambda ?? 'N/A'))}
      &nbsp;·&nbsp;
      Energy: <span class="chip chip-dim">${escHTML((data.energy||{}).label || 'UNAVAILABLE')}</span>
    </div>
  `;

  setHTML('bvir-verdict', verdictHTML);
  show('bvir-verdict');

  const outputData = {
    decision: data.decision,
    'governance.lambda': (data.governance||{}).lambda,
    'governance.lambda_kind': (data.governance||{}).lambda_kind,
    'receipt.seq': receipt.seq,
    'receipt.prev': String(chainPrev).substring(0,32) + '…',
    'receipt.digest': String(chainDigest).substring(0,32) + '…',
    'dsse.signed': dsse.signed,
    'dsse.keyid': dsseKeyid || null,
    'dsse.key_kind': isDemoKey ? 'demo (demo-signing-key — NOT production cosign)' : (dsse.signed ? 'production cosign' : null),
    'dsse.payloadType': dsse.payloadType,
    'verify.public_key_url': pubKeyURL,
    'verify.computed_payload_sha256': payloadDigestComputed.substring(0,32) + '…',
    'verify.declared_payload_digest': hasDeclaredDigest ? declaredPayloadDigest.substring(0,32) + '…' : null,
    'verify.payload_digest_match': hasDeclaredDigest ? (payloadDigestMatches ? 'MATCH' : 'MISMATCH') : 'no declared digest to compare',
    'verify.pae_sha256': paeSHA.substring(0,32) + '…',
    'verify.result': verified ? (isDemoKey ? 'VERIFIED ✓ (demo-signing-key — not production cosign)' : 'VERIFIED ✓') : (dsse.signed === false ? 'UNSIGNED (no private key in runtime)' : 'FAILED: ' + verifyError),
    'energy.label': (data.energy||{}).label,
  };
  el('bvir-output').textContent = JSON.stringify(outputData, null, 2);
  show('bvir-output');
  el('bvir-output').className = 'output ' + (verified ? 'verified' : (dsse.signed === false ? '' : 'failed'));

  setStatus('bvir-status', verified
    ? (isDemoKey
        ? '✓ WebCrypto verified — real ECDSA-P256 over DSSE PAE with demo-signing-key (NOT the production cosign key).'
        : '✓ WebCrypto verified — real ECDSA-P256 signature over DSSE PAE.')
    : (dsse.signed === false
        ? 'Unsigned receipt (private key absent from runtime). Chain valid.'
        : 'Verification result: ' + verifyError));
  btn.disabled = false;
}

/* ====================================================================
   SECTION B — Governed Refusal
   ==================================================================== */
async function runGovern(caseKey) {
  hide('govern-panel');
  setStatus('govern-status', `Calling /api/a11oy/v1/demo/govern case="${caseKey}" …`, true);

  let data;
  try {
    const resp = await fetch('/api/a11oy/v1/demo/govern', {
      method: 'POST',
      headers: { 'Content-Type': 'application/json' },
      body: JSON.stringify({ case: caseKey })
    });
    data = await resp.json();
  } catch(e) {
    setStatus('govern-status', 'Error: ' + e.message);
    return;
  }

  const gov     = data.governance || {};
  const receipt = data.receipt    || {};
  const dsse    = data.dsse       || {};
  const chain   = data.chain      || {};
  const decision = data.decision  || caseKey;

  // Verdict banner
  const decClasses = { allow:'verdict-ok', review:'verdict-dim', deny:'verdict-fail' };
  const decLabels  = { allow:'✓ ALLOW — governance passed', review:'⚠ REVIEW — below advisory floor', deny:'✗ DENY — gate fired' };
  const bannerCls  = decClasses[decision] || 'verdict-dim';
  const bannerLbl  = decLabels[decision]  || decision.toUpperCase();
  el('govern-verdict-banner').innerHTML = `<div class="verdict-banner ${bannerCls}">${bannerLbl}</div>`;

  // Λ row
  const lambdaPass = gov.lambda_pass;
  el('govern-lambda-row').innerHTML = `
    <div style="display:flex;align-items:center;gap:10px;flex-wrap:wrap">
      <span style="font-size:14px;font-weight:700">Λ = ${escHTML(String(gov.lambda ?? 'N/A'))}</span>
      <span class="chip ${lambdaPass ? 'chip-ok' : 'chip-err'}">
        ${lambdaPass ? 'PASS' : 'FAIL'} (floor ${escHTML(String(gov.lambda_floor ?? 0.9))})
      </span>
      <span class="conj">Conjecture 1 — advisory, NOT a theorem</span>
    </div>
    <div style="font-size:12px;color:var(--text-dim);margin-top:4px">
      ${escHTML(gov.lambda_kind || 'Conjecture 1 (advisory; NOT a theorem)')}
    </div>
  `;

  // Gates
  const gates = gov.gates || [];
  let gatesHTML = `<div style="font-size:11px;font-weight:700;text-transform:uppercase;letter-spacing:.07em;color:var(--text-dim);margin-bottom:8px">Gates</div>`;
  gates.forEach(g => {
    const fired = g.fired;
    gatesHTML += `
      <div class="gate-row">
        <span class="gate-name">${escHTML(g.name || '—')}</span>
        <span class="gate-fired ${fired ? 'chip chip-err' : 'chip chip-ok'}">${fired ? 'FIRED' : 'PASS'}</span>
        <span class="chip chip-dim">${escHTML(g.decision || '—')}</span>
      </div>`;
  });
  el('govern-gates').innerHTML = gatesHTML;

  // Signed receipt on deny
  if (decision === 'deny' || decision === 'review') {
    const signed = dsse.signed;
    const receiptOut = {
      decision: receipt.decision,
      seq: receipt.seq,
      lambda: receipt.lambda,
      lambda_kind: receipt.lambda_kind,
      gates: receipt.gates,
      prev: String(chain.prev || '').substring(0,32) + '…',
      digest: String(chain.digest || '').substring(0,32) + '…',
      'dsse.signed': signed,
      'dsse.keyid': ((dsse.signatures||[])[0]||{}).keyid,
      honesty: data.honesty,
    };
    el('govern-receipt-output').className = 'output ' + (signed ? 'verified' : '');
    el('govern-receipt-output').textContent = JSON.stringify(receiptOut, null, 2);
    show('govern-receipt-block');
  } else {
    hide('govern-receipt-block');
  }

  show('govern-panel');
  setStatus('govern-status', `Decision: ${decision.toUpperCase()} · Λ = ${gov.lambda} · ${dsse.signed ? 'Receipt signed ✓' : 'Receipt unsigned (key absent)'}`);
}

/* ====================================================================
   SECTION C — Verifiable Thesis
   ==================================================================== */
async function loadThesis() {
  const btn = el('thesis-load');
  btn.disabled = true;
  hide('thesis-panel');
  setStatus('thesis-status', 'Loading /api/a11oy/v1/demo/thesis …', true);

  let data;
  try {
    const resp = await fetch('/api/a11oy/v1/demo/thesis');
    data = await resp.json();
  } catch(e) {
    setStatus('thesis-status', 'Error: ' + e.message);
    btn.disabled = false;
    return;
  }

  const corpus   = data.corpus   || {};
  const formulas = data.formulas || [];
  const doctrine = data.doctrine_static || {};

  // ---- Corpus diagram ----
  const tiers = corpus.tiers || [];
  const corpusColors = ['proven','gates','total'];
  let corpusHTML = `<div style="font-size:13px;font-weight:700;margin-bottom:14px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em">3-Tier Honest Corpus</div>`;
  corpusHTML += `<div class="corpus-diagram">`;
  tiers.forEach((t, idx) => {
    corpusHTML += `
      <div class="corpus-tier">
        <div class="corpus-count ${corpusColors[idx] || ''}">${escHTML(String(t.count))}</div>
        <div class="corpus-tier-label">${escHTML(t.label || '')}</div>
        <div class="corpus-tier-desc">${escHTML(t.description || '')}</div>
      </div>`;
  });
  corpusHTML += `</div>`;
  corpusHTML += `<div class="corpus-never-claim">
    ⚠ ${escHTML(corpus.honest_note || 'We never claim 183 proven.')}
  </div>`;
  el('thesis-corpus').innerHTML = corpusHTML;

  // ---- 8 formulas ----
  let formulasHTML = '';
  formulas.forEach(f => {
    formulasHTML += `
      <div class="formula-card">
        <div class="formula-card-head">
          <span class="formula-id">${escHTML(f.id)}</span>
          <span class="formula-name">${escHTML(f.name)}</span>
        </div>
        <div class="formula-lean">${escHTML(f.lean)}</div>
        <div class="formula-desc">${escHTML(f.description)}</div>
        <div class="formula-status">✓ ${escHTML(f.status)}</div>
      </div>`;
  });
  el('thesis-formulas').innerHTML = formulasHTML;

  // ---- Conjecture labels ----
  el('thesis-conjectures').innerHTML = `
    <div style="font-size:13px;font-weight:700;margin-bottom:12px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em">
      Advisory / Conjecture Labels
    </div>
    <div style="display:flex;gap:14px;flex-wrap:wrap">
      <div style="flex:1;min-width:220px;background:var(--bg-panel);border:1px solid #92400e;border-radius:var(--radius);padding:14px">
        <div style="font-size:11px;font-weight:700;color:var(--amber);text-transform:uppercase;letter-spacing:.07em;margin-bottom:6px">Conjecture 1 — Λ (Lambda)</div>
        <div style="font-size:13px;color:var(--text-dim)">${escHTML(doctrine.lambda_kind || 'Conjecture 1 (advisory; NOT a theorem)')}</div>
        <div style="font-size:12px;color:var(--text-mute);margin-top:6px">Open bounty: szl-holdings/lambda-bounty</div>
      </div>
      <div style="flex:1;min-width:220px;background:var(--bg-panel);border:1px solid #991b1b;border-radius:var(--radius);padding:14px">
        <div style="font-size:11px;font-weight:700;color:var(--red);text-transform:uppercase;letter-spacing:.07em;margin-bottom:6px">Conjecture 2 — Khipu BFT</div>
        <div style="font-size:13px;color:var(--text-dim)">${escHTML(doctrine.bft_kind || 'Conjecture 2 (NOT proven; NOT a theorem)')}</div>
        <div style="font-size:12px;color:var(--text-mute);margin-top:6px">Labeled honestly everywhere — no false safety claim</div>
      </div>
    </div>
    <div style="margin-top:14px;font-size:12px;color:var(--text-dim)">
      ${escHTML(doctrine.moat_line || '')}
    </div>
  `;

  show('thesis-panel');
  setStatus('thesis-status', `Loaded ${formulas.length} proven formulas · 3-tier corpus · live doctrine`);
  btn.disabled = false;
}

/* ====================================================================
   SECTION D — Public Ledger (real receipts from szl-lake, snapshot)
   In-browser: hash-chain linkage check. Offline: signatures via szl-receipt.
   ==================================================================== */
const LEDGER_SNAPSHOT = {"source": "https://huggingface.co/datasets/SZLHOLDINGS/szl-lake", "captured_utc": "2026-07-02", "lutar_lean": [{"branch": "theorem-u-kernel", "chain_index": 1, "doctrine": "v11", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated. Theorem U does NOT close it.", "doctrine": "v11", "locked_five_unchanged": true, "locked_set": ["F1", "F11", "F12", "F18", "F19"], "theorem_u": "REAL-conditional: Lutar.Uniqueness Theorem U is kernel-verified (axiom footprint within the Lean/Mathlib trust base, no sorry) but CONDITIONAL on its stated checkable hypotheses; it is NOT part of the locked-proven baseline."}, "kernel_commit": "e736decd244ae06e8bb48531c6c7dc0f1029b25a", "kernel_commit_short": "e736decd244a", "kind": "theorem-u-anchor", "lambda_status": "Conjecture_1 (OPEN; unconditional uniqueness machine-checked FALSE)", "numbers": {"axioms_unique": 22, "declarations": 1323, "sorries_noncomment": 254}, "organ": "lutar-lean", "prev_hash": null, "receipt_id": "d70f444db57df9a4a2d52e69408ce61b511e4b50152f7fbf97456b1af66fe9a0", "schema": "szl.khipu.receipt/v1", "signing": {"format": "sigstore-keyless-bundle", "bytes": 18428, "b64_head": "eyJtZWRpYVR5cGUiOiJhcHBsaWNhdGlvbi92bmQuZGV2\u2026"}, "source_run": {"conclusion": "success", "id": "27186151340", "url": "https://github.com/szl-holdings/lutar-lean/actions/runs/27186151340", "workflow": "Lake build (gate + numbers)"}, "subject": {"name": "theorem_u_snapshot.json", "sha256": "82d08a4e892579e815d880d51f61cb8035a3325e077c29e412f310f76b50985e", "snapshot": {"branch": "theorem-u-kernel", "built_at_utc": "2026-06-09T05:37:45Z", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated. Theorem U does NOT close it.", "doctrine": "v11", "locked_five_unchanged": true, "locked_set": ["F1", "F11", "F12", "F18", "F19"], "theorem_u": "REAL-conditional: Lutar.Uniqueness Theorem U is kernel-verified (axiom footprint within the Lean/Mathlib trust base, no sorry) but CONDITIONAL on its stated checkable hypotheses; it is NOT part of the locked-proven baseline."}, "kernel_commit": "e736decd244ae06e8bb48531c6c7dc0f1029b25a", "kernel_commit_short": "e736decd244a", "lean_numbers": {"lean_numbers_sha256": "50098073e92aefdf275ec53e60faafc0f1bd5d4a1a88023e819490aaaa69d4d6", "numbers": {"axiom_names": ["A6'_block_consistent", "KS_theorem_1_1", "MomentSubGaussian", "audit_reidemeister_invariance", "canonicalReceipt", "chromotopology_code_bijection", "compression_collision_resistant", "domain_separation", "gleason_length_mod_8", "klDivergence_nonneg", "lambda_schur_concave_n_axis", "lambda_stationary_unique", "leaf_collision_resistant", "liu_hui_pi_converges", "node_collision_resistant", "pinsker", "r1_invariance", "r2_invariance", "setAlpha_cauchy", "setDelta_stage2", "sha256", "sha256_collision_resistant"], "axioms_raw": 23, "axioms_unique": 22, "declarations": 1323, "sorries_baseline": 251, "sorries_noncomment": 254, "sorries_putnam": 56, "sorries_raw": 307}, "reference_vectors_sha256": "857967629daf5e5c45a167306ea0e0091569a29766b01ac91bef15a539b816dc", "replay_hash": "9860c3332a2d0b0553b775dcd27111b0ce4fae4bc5cebe2827dc6148be4cbebe", "schema": "szl.lean_numbers/v1"}, "repo": "szl-holdings/lutar-lean", "schema": "szl.theorem_u.snapshot/v1", "theorem_u": {"decl_source_sha256": {"Lutar/Uniqueness/AxiomCheck.lean": "f45781ef2becf15eccd0c31702603a55cfab1eb7960483593a045202b66f4887", "Lutar/Uniqueness/Identifiability.lean": "fa340e6a999eac7ea1cd035d90647548baaa290b7376d7fcbdcbd165e475dedf", "Lutar/Uniqueness/LambdaEquiv.lean": "03f63e36f3a9b19e8e9d4f48313a450bae7c85fcb53049d52e0f6d4adf4b1c23", "Lutar/Uniqueness/TheoremU.lean": "c958520ba31d6fc1f48a9b49871d67812f178e168b31bf2be9e3d5fb2061386c"}, "full_axiom_footprint": {"Lutar.Uniqueness.AxiomCheck.conjecture1_still_open": [], "Lutar.Uniqueness.AxiomCheck.locked_count_five": [], "Lutar.Uniqueness.AxiomCheck.theoremU_axiom_sets_kernel_only": [], "Lutar.Uniqueness.AxiomCheck.theoremU_excluded_from_locked": [], "Lutar.Uniqueness.CorollaryU1_LambdaUnique_Separable": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.CorollaryU2_LambdaUnique_Factors": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique_eq": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.identifiability_forces_lambda": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.lambda_equiv_to_eq_of_anchored": ["Classical.choice", "Quot.sound", "propext"]}, "headline_axiom_footprint": {"CorollaryU1_LambdaUnique_Separable": ["Classical.choice", "Quot.sound", "propext"], "CorollaryU2_LambdaUnique_Factors": ["Classical.choice", "Quot.sound", "propext"], "TheoremU_LambdaUnique": ["Classical.choice", "Quot.sound", "propext"], "TheoremU_LambdaUnique_eq": ["Classical.choice", "Quot.sound", "propext"], "identifiability_forces_lambda": ["Classical.choice", "Quot.sound", "propext"], "lambda_equiv_to_eq_of_anchored": ["Classical.choice", "Quot.sound", "propext"]}, "headline_decls": ["CorollaryU1_LambdaUnique_Separable", "CorollaryU2_LambdaUnique_Factors", "TheoremU_LambdaUnique", "TheoremU_LambdaUnique_eq", "identifiability_forces_lambda", "lambda_equiv_to_eq_of_anchored"], "kernel_only": true, "kernel_trust_base": ["Classical.choice", "Quot.sound", "funext", "propext"], "module": "Lutar.Uniqueness", "status": "REAL-conditional"}}}, "theorem_u_status": "REAL-conditional", "timestamp": "2026-06-09T05:39:22Z"}, {"branch": "main", "chain_index": 2, "doctrine": "v11", "honesty": {"conjecture": "This is a GENERATED, OPEN conjecture \u2014 NOT a theorem and NOT machine-verified. It remains OPEN until a solution is independently verified.", "difficulty": "Difficulty 'open-resistant' / grade 'OPEN' come from a REAL bounded solver run. OPEN means searched-to-budget, not proven true; VERIFIED-FINITE certifies only the finite enumerated domain; REFUTED carries a concrete witness. No score is fabricated.", "doctrine": "v11", "kernel_only": false, "novelty": "Novelty verdict 'novel-candidate' is an advisory screen, not a proof of originality; external prior-art sources are labelled live/cached/unreachable and an unreachable source never confirms novelty.", "signing": "Disclosure is cosign keyless-OIDC signed and anchored into the szl-lake DSSE Khipu ledger; the signature attests the timestamp + content, NOT the truth of the conjecture.", "status": "OPEN"}, "kernel_commit": "d851aefe86b9f12f9d4423200bd9e5257d05c41e", "kernel_commit_short": "d851aefe86b9", "kind": "conjecture-disclosure-anchor", "milestone_kind": "conjecture-disclosure", "milestone_status": "OPEN", "milestone_title": "SZL mixing-map convergence conjecture", "numbers": {"axioms_unique": null, "declarations": null, "sorries_noncomment": null}, "organ": "lutar-lean", "prev_hash": "d70f444db57df9a4a2d52e69408ce61b511e4b50152f7fbf97456b1af66fe9a0", "receipt_id": "08744b67b647039f87abbf0b29587638ae777308ca7fc2434ed3ae4033687b50", "schema": "szl.khipu.receipt/v1", "signing": {"format": "sigstore-keyless-bundle", "bytes": 17488, "b64_head": "eyJtZWRpYVR5cGUiOiJhcHBsaWNhdGlvbi92bmQuZGV2\u2026"}, "source_run": {"conclusion": "success", "id": "27318564784", "url": "https://github.com/szl-holdings/lutar-lean/actions/runs/27318564784", "workflow": "Conjecture Factory (generate -> timestamp -> grade -> anchor)"}, "subject": {"name": "conjecture_snapshot.json", "sha256": "7faded7df9ac5bea4ca7ddaa1e5c38c247c237fd49b8a1a39d35a260c2189fb0", "snapshot": {"branch": "main", "built_at_utc": "2026-06-11T01:54:20Z", "candidate": {"created_utc": "2026-06-11T01:54:19Z", "doctrine": "v11", "domain": "number-theory / arithmetic dynamics", "id": "cf-5ddbbe7571a9", "intended_solution_outline": "Bound the orbit by a Lyapunov / drift argument on the 2-adic valuation: show the\ncontracting branch (n = 3 mod 4) dominates the accelerating branch (n = 1 mod 4)\nin expectation, then rule out non-trivial cycles via a residue-class descent.\nStatus: OPEN \u2014 no proof is claimed; the predicate only performs bounded testing.", "predicate": {"description": "Sound bounded-orbit checker: returns False only on a detected non-1 cycle (a certain counterexample); inconclusive bounded runs assert no counterexample.", "entry": "holds", "kind": "python-callable", "module": "conjectures/samples/szl-mixing-map/predicate.py"}, "references": ["conjectures/corpus/collatz.md (related but distinct: classical 3n+1 map)", "Lagarias, J. (2010). The 3x+1 problem: an annotated bibliography."], "schema": "szl.conjecture.candidate/v1", "statement": "Define M : Z+ -> Z+ by\n    M(n) = n / 2          if n is even,\n    M(n) = (3n + 1) / 2    if n is odd and n = 1 (mod 4),\n    M(n) = (n + 1) / 2     if n is odd and n = 3 (mod 4).\nConjecture: for every integer n >= 1 there exists k >= 0 with M^k(n) = 1.", "statement_canonical": "Define M : Z+ -> Z+ by M(n) = n / 2 if n is even, M(n) = (3n + 1) / 2 if n is odd and n = 1 (mod 4), M(n) = (n + 1) / 2 if n is odd and n = 3 (mod 4). Conjecture: for every integer n >= 1 there exists k >= 0 with M^k(n) = 1.", "statement_hash": "sha256:5ddbbe7571a93f9ed3d49c37dbb3559eb339a51380e427882bd3783b7cb2743a", "taxonomy": "OPEN", "title": "SZL mixing-map convergence conjecture"}, "grade": {"budget": 100000, "candidate_id": "cf-5ddbbe7571a9", "difficulty": "open-resistant", "graded_utc": "2026-06-11T01:54:20Z", "honesty": "Grade from a REAL ensemble run. REFUTED carries a concrete witness. VERIFIED-FINITE certifies only the finite enumerated domain, not the conjecture in general. OPEN means searched-to-budget with no counterexample \u2014 NOT a proof of truth. The candidate stays OPEN (doctrine v11).", "result": "OPEN", "schema": "szl.conjecture.grade/v1", "seed": 1729, "solver_ensemble": [{"budget": 100000, "checked": 100000, "elapsed_sec": 0.411268, "note": "infinite/streaming domain", "resolved": false, "result": "OPEN", "solver": "exhaustive", "witness": null}, {"budget": 100000, "checked": 100000, "elapsed_sec": 0.654207, "note": "random sampling found no counterexample (not a proof)", "resolved": false, "result": "OPEN", "solver": "sampler", "witness": null}], "success_rate": 0.0, "witness": null}, "honesty": {"conjecture": "This is a GENERATED, OPEN conjecture \u2014 NOT a theorem and NOT machine-verified. It remains OPEN until a solution is independently verified.", "difficulty": "Difficulty 'open-resistant' / grade 'OPEN' come from a REAL bounded solver run. OPEN means searched-to-budget, not proven true; VERIFIED-FINITE certifies only the finite enumerated domain; REFUTED carries a concrete witness. No score is fabricated.", "doctrine": "v11", "kernel_only": false, "novelty": "Novelty verdict 'novel-candidate' is an advisory screen, not a proof of originality; external prior-art sources are labelled live/cached/unreachable and an unreachable source never confirms novelty.", "signing": "Disclosure is cosign keyless-OIDC signed and anchored into the szl-lake DSSE Khipu ledger; the signature attests the timestamp + content, NOT the truth of the conjecture.", "status": "OPEN"}, "kernel_commit": "d851aefe86b9f12f9d4423200bd9e5257d05c41e", "kernel_commit_short": "d851aefe86b9", "kind": "conjecture-disclosure", "milestone": {"difficulty": "open-resistant", "grade_result": "OPEN", "headline_decls": [], "id": "cf-5ddbbe7571a9", "kernel_only": false, "novelty_verdict": "novel-candidate", "release_stage": "statement", "statement_hash": "sha256:5ddbbe7571a93f9ed3d49c37dbb3559eb339a51380e427882bd3783b7cb2743a", "status": "OPEN", "title": "SZL mixing-map convergence conjecture"}, "novelty": {"candidate_id": "cf-5ddbbe7571a9", "external": [{"hits": 0, "note": "offline run (--online not set)", "source": "arxiv", "status": "unreachable", "top": []}, {"hits": 0, "note": "offline run (--online not set)", "source": "crossref", "status": "unreachable", "top": []}], "honesty": "Novelty is a screen, not a proof of originality. External sources are labelled live/cached/unreachable; an unreachable source contributes no hits and is never silently treated as confirming novelty. The candidate stays OPEN regardless of this verdict (doctrine v11).", "local_corpus": {"corpus_dir": "conjectures/corpus", "documents_scanned": 2, "max_similarity": 0.0688, "method": "char-5-gram shingle Jaccard", "near_duplicate": false, "nearest": {"doc": "collatz.md", "similarity": 0.0688}, "threshold": 0.8, "top": [{"doc": "collatz.md", "similarity": 0.0688}, {"doc": "goldbach.md", "similarity": 0.0451}]}, "schema": "szl.conjecture.novelty/v1", "screened_utc": "2026-06-11T01:54:19Z", "statement_hash": "sha256:5ddbbe7571a93f9ed3d49c37dbb3559eb339a51380e427882bd3783b7cb2743a", "verdict": "novel-candidate", "verdict_reason": "no near-duplicate found (local-only; external prior-art not fully screened \u2014 unreachable: ['arxiv', 'crossref'])"}, "predicate_type": "https://szl-holdings/conjecture-disclosure/v1", "repo": "szl-holdings/lutar-lean", "schema": "szl.conjecture.disclosure/v1"}}, "timestamp": "2026-06-11T01:54:27Z"}, {"branch": "main", "chain_index": 3, "doctrine": "v11", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated; conjecture1_still_open re-asserts it stays open.", "doctrine": "v11", "locked_baseline": "REAL-invariant: kernel-verified meta-theorems in Lutar/Uniqueness/AxiomCheck.lean (locked_count_eight, theoremU_excluded_from_locked, theoremU_axiom_sets_kernel_only, conjecture1_still_open) \u2014 each proven by `decide`, axiom footprint within the Lean/Mathlib trust base, no sorry. They ASSERT that the locked-proven baseline is EXACTLY the eight {F1,F4,F7,F11,F12,F18,F19,F22}; they do NOT themselves re-prove those formulas (the formula proofs live in Lutar/Puriq/Formulas/ProvedFormulas.lean).", "locked_set": ["F1", "F4", "F7", "F11", "F12", "F18", "F19", "F22"], "theorem_u": "Theorem U stays REAL-conditional and EXCLUDED from this locked baseline (theoremU_excluded_from_locked); anchoring this milestone does not change Theorem U's status."}, "kernel_commit": "25e0b2af781f5fb10324945ea10c861bcc28cc83", "kernel_commit_short": "25e0b2af781f", "kind": "locked-baseline-anchor", "milestone_kind": "locked-baseline", "milestone_status": "REAL-invariant", "milestone_title": "Locked-proven baseline (Doctrine v11) \u2014 kernel meta-invariants", "numbers": {"axioms_unique": 22, "declarations": 1323, "sorries_noncomment": 254}, "organ": "lutar-lean", "prev_hash": "08744b67b647039f87abbf0b29587638ae777308ca7fc2434ed3ae4033687b50", "receipt_id": "dcdad01763241e4d7af6b45e59949e6596c12ccf43ed6b784471c1f05b4715c0", "schema": "szl.khipu.receipt/v1", "signing": {"format": "sigstore-keyless-bundle", "bytes": 19036, "b64_head": "eyJtZWRpYVR5cGUiOiJhcHBsaWNhdGlvbi92bmQuZGV2\u2026"}, "source_run": {"conclusion": "success", "id": "27319352318", "url": "https://github.com/szl-holdings/lutar-lean/actions/runs/27319352318", "workflow": "Lake build (gate + numbers)"}, "subject": {"name": "locked_baseline_snapshot.json", "sha256": "19ea5946195f7437cfb881eb5489898d0d45f5f074dfa210c22eb6c8bbfc3bc9", "snapshot": {"branch": "main", "built_at_utc": "2026-06-11T02:18:27Z", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated; conjecture1_still_open re-asserts it stays open.", "doctrine": "v11", "locked_baseline": "REAL-invariant: kernel-verified meta-theorems in Lutar/Uniqueness/AxiomCheck.lean (locked_count_eight, theoremU_excluded_from_locked, theoremU_axiom_sets_kernel_only, conjecture1_still_open) \u2014 each proven by `decide`, axiom footprint within the Lean/Mathlib trust base, no sorry. They ASSERT that the locked-proven baseline is EXACTLY the eight {F1,F4,F7,F11,F12,F18,F19,F22}; they do NOT themselves re-prove those formulas (the formula proofs live in Lutar/Puriq/Formulas/ProvedFormulas.lean).", "locked_set": ["F1", "F4", "F7", "F11", "F12", "F18", "F19", "F22"], "theorem_u": "Theorem U stays REAL-conditional and EXCLUDED from this locked baseline (theoremU_excluded_from_locked); anchoring this milestone does not change Theorem U's status."}, "kernel_commit": "25e0b2af781f5fb10324945ea10c861bcc28cc83", "kernel_commit_short": "25e0b2af781f", "kind": "locked-baseline", "lean_numbers": {"lean_numbers_sha256": "38f9a69cb289110e44ffa9bc4a8575d811220c4654a7985b85694d6f1bb3f7f9", "numbers": {"axiom_names": ["A6'_block_consistent", "KS_theorem_1_1", "MomentSubGaussian", "audit_reidemeister_invariance", "canonicalReceipt", "chromotopology_code_bijection", "compression_collision_resistant", "domain_separation", "gleason_length_mod_8", "klDivergence_nonneg", "lambda_schur_concave_n_axis", "lambda_stationary_unique", "leaf_collision_resistant", "liu_hui_pi_converges", "node_collision_resistant", "pinsker", "r1_invariance", "r2_invariance", "setAlpha_cauchy", "setDelta_stage2", "sha256", "sha256_collision_resistant"], "axioms_raw": 23, "axioms_unique": 22, "declarations": 1323, "sorries_baseline": 251, "sorries_noncomment": 254, "sorries_putnam": 56, "sorries_raw": 307}, "reference_vectors_sha256": "857967629daf5e5c45a167306ea0e0091569a29766b01ac91bef15a539b816dc", "replay_hash": "1f0c9d9938b96b3d56fe01e37b955e1b91ff1aec0610fe30c30e515cc8ab469c", "schema": "szl.lean_numbers/v1"}, "milestone": {"decl_source_sha256": {"Lutar/Uniqueness/AxiomCheck.lean": "5e7998d33a1928c12f2e07595ec929544ac04e37f17ad7693ab2838136ab540f", "Lutar/Uniqueness/Identifiability.lean": "fa340e6a999eac7ea1cd035d90647548baaa290b7376d7fcbdcbd165e475dedf", "Lutar/Uniqueness/LambdaEquiv.lean": "03f63e36f3a9b19e8e9d4f48313a450bae7c85fcb53049d52e0f6d4adf4b1c23", "Lutar/Uniqueness/TheoremU.lean": "c958520ba31d6fc1f48a9b49871d67812f178e168b31bf2be9e3d5fb2061386c"}, "full_axiom_footprint": {"Lutar.Uniqueness.AxiomCheck.conjecture1_still_open": [], "Lutar.Uniqueness.AxiomCheck.locked_count_eight": [], "Lutar.Uniqueness.AxiomCheck.theoremU_axiom_sets_kernel_only": [], "Lutar.Uniqueness.AxiomCheck.theoremU_excluded_from_locked": [], "Lutar.Uniqueness.CorollaryU1_LambdaUnique_Separable": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.CorollaryU2_LambdaUnique_Factors": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique_eq": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.identifiability_forces_lambda": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.lambda_equiv_to_eq_of_anchored": ["Classical.choice", "Quot.sound", "propext"]}, "headline_axiom_footprint": {"conjecture1_still_open": [], "locked_count_eight": [], "theoremU_axiom_sets_kernel_only": [], "theoremU_excluded_from_locked": []}, "headline_decls": ["conjecture1_still_open", "locked_count_eight", "theoremU_axiom_sets_kernel_only", "theoremU_excluded_from_locked"], "id": "locked-baseline", "kernel_only": true, "kernel_trust_base": ["Classical.choice", "Quot.sound", "funext", "propext"], "module": "Lutar.Uniqueness.AxiomCheck", "status": "REAL-invariant", "title": "Locked-proven baseline (Doctrine v11) \u2014 kernel meta-invariants"}, "repo": "szl-holdings/lutar-lean", "schema": "szl.proof.snapshot/v1"}}, "timestamp": "2026-06-11T02:20:21Z"}], "amaru": [{"receipt_id": "4c9c3f2b8d6452d9bc0e9a9144fc9e1743b3ca76544a988d4d9e4b39df87ba73", "timestamp": "2026-06-02T02:13:07.827680+00:00", "organ": "amaru", "kind": "tick", "index": 0, "lambda": 0.9, "lambda_pass": true, "predicted_hash": "", "actual_hash": "4c9c3f2b8d6452d9bc0e9a9144fc9e1743b3ca76544a988d4d9e4b39df87ba73", "delta": 0.0, "lutar_anchor": "c7c0ba17", "doctrine": "v11", "decl": 749, "axioms": 14, "sorries": 163, "neuro_citations": "[]", "dsse_payload_type": "application/vnd.szl.khipu+json", "dsse_pae_sha256": "6a8ba013ddcd1938e0fc2174ef79287ca49266277b0195595f324dacb9eb02c9", "dsse_sig": "MEQCIBIZjd6T0E4Bhl0OGkhcMZmAuqmnN0ZxmWrL+7U/h31JAiAmF2U1DBEQieaDrFkHcjBcOW91PY1glK0X+/2EKprpVQ==", "dsse_keyid": "szlholdings-cosign", "dsse_signed": true, "verify_key_url": "https://github.com/szl-holdings/.github/blob/main/cosign.pub"}, {"receipt_id": "bc4d6a1629c01584eb6789d19a432fbc9448ce92ada8d47e14552fe94dee9fa1", "timestamp": "2026-06-02T02:13:08.490579+00:00", "organ": "amaru", "kind": "tick", "index": 1, "lambda": 0.9, "lambda_pass": true, "predicted_hash": "4c9c3f2b8d6452d9bc0e9a9144fc9e1743b3ca76544a988d4d9e4b39df87ba73", "actual_hash": "bc4d6a1629c01584eb6789d19a432fbc9448ce92ada8d47e14552fe94dee9fa1", "delta": 0.0, "lutar_anchor": "c7c0ba17", "doctrine": "v11", "decl": 749, "axioms": 14, "sorries": 163, "neuro_citations": "[]", "dsse_payload_type": "application/vnd.szl.khipu+json", "dsse_pae_sha256": "3cb923bc57002b34cd52124601bfbeeff68c6232e598dd06eccb4ff2847f1371", "dsse_sig": "MEUCIQDBB4xUJMFm4YKcZ0mcz6n3q6XomOKEepJWmaplX9Xo0gIgUIg3Xm316oVN05pvIoNxhJBDyL6Vhp1xfEq9nx9V5Wg=", "dsse_keyid": "szlholdings-cosign", "dsse_signed": true, "verify_key_url": "https://github.com/szl-holdings/.github/blob/main/cosign.pub"}, {"receipt_id": "2f872c5144585602dd1016ce732912134ad30423e442fda009cdc0d168c6732d", "timestamp": "2026-06-02T02:13:09.173270+00:00", "organ": "amaru", "kind": "tick", "index": 2, "lambda": 0.9, "lambda_pass": true, "predicted_hash": "bc4d6a1629c01584eb6789d19a432fbc9448ce92ada8d47e14552fe94dee9fa1", "actual_hash": "2f872c5144585602dd1016ce732912134ad30423e442fda009cdc0d168c6732d", "delta": 0.0, "lutar_anchor": "c7c0ba17", "doctrine": "v11", "decl": 749, "axioms": 14, "sorries": 163, "neuro_citations": "[]", "dsse_payload_type": "application/vnd.szl.khipu+json", "dsse_pae_sha256": "f72e37f1ea8d785d862ec7469d3908fc7b455360964d6cdea61e430d89b3e66d", "dsse_sig": "MEYCIQDvfS5l1nyk5zHz9wsNwe/wj6ZPNAMbbJ4KzMG2ZXEQkwIhAJ4mkTOAnOdNWFb2SuweFbQnjP0QPORGAA/IU8sHB+X5", "dsse_keyid": "szlholdings-cosign", "dsse_signed": true, "verify_key_url": "https://github.com/szl-holdings/.github/blob/main/cosign.pub"}]};

function renderLedger() {
  const btn = el('ledger-load');
  btn.disabled = true;
  setStatus('ledger-status', 'Checking hash-chain linkage in-browser …', true);

  const lut = LEDGER_SNAPSHOT.lutar_lean || [];
  const ama = LEDGER_SNAPSHOT.amaru || [];
  const hfBase = 'https://huggingface.co/datasets/SZLHOLDINGS/szl-lake/blob/main/khipu/';

  let links = 0, broken = 0;
  const rows = lut.map((r, i) => {
    const prev = r.prev_hash;
    const ok = (i === 0) ? (prev === null || prev === '' || prev === undefined)
                         : (prev === lut[i-1].receipt_id);
    if (ok) links++; else broken++;
    return { r, i, prev, ok };
  });
  const intact = broken === 0;
  let chainHTML = '<div class="verdict-banner ' + (intact ? 'verdict-ok' : 'verdict-fail') + '">'
    + (intact ? '✓ CHAIN INTACT' : '✗ CHAIN BROKEN') + ' — ' + links + '/' + lut.length
    + ' hash-links verified in your browser <span class="chip chip-dim">organ: lutar-lean</span></div>'
    + '<div style="font-size:12px;color:var(--text-dim);margin-bottom:8px">Each receipt\'s <code>prev_hash</code> '
    + 'is compared to the previous receipt\'s <code>receipt_id</code>. This proves append-only ordering. '
    + 'Content-hash and signature verification run offline via szl-receipt.</div>';
  rows.forEach(({ r, i, prev, ok }) => {
    chainHTML += '<div class="hash-row"><span class="hash-label">#' + escHTML(String(r.chain_index)) + ' '
      + escHTML(r.kind || '') + '</span><span class="hash-val">id ' + escHTML(String(r.receipt_id).substring(0,16))
      + '…</span><span class="hash-val ' + (ok ? 'hash-match' : 'hash-mismatch') + '">prev '
      + escHTML(prev == null ? '(genesis)' : String(prev).substring(0,16) + '…') + '</span>'
      + '<span class="chip ' + (ok ? 'chip-ok' : 'chip-err') + '">' + (ok ? 'LINK OK' : 'BROKEN') + '</span></div>';
  });
  el('ledger-chain').innerHTML = chainHTML;

  let cardsHTML = '<div style="font-size:13px;font-weight:700;margin-bottom:14px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em">Receipts (verbatim honesty labels)</div>';
  lut.forEach(r => {
    const h = r.honesty || {};
    let honestyHTML = '';
    Object.keys(h).forEach(k => {
      const v = h[k];
      if (typeof v === 'string') {
        honestyHTML += '<div style="margin:4px 0"><span class="chip chip-warn">' + escHTML(k) + '</span> '
          + '<span style="font-size:12px;color:var(--text-dim)">' + escHTML(v) + '</span></div>';
      }
    });
    const sg = r.signing || {};
    cardsHTML += '<div class="formula-card"><div class="formula-card-head">'
      + '<span class="formula-id">lutar-lean</span><span class="formula-name">' + escHTML(r.kind || 'receipt') + '</span>'
      + '<span class="chip chip-dim">schema ' + escHTML(r.schema || '') + '</span></div>'
      + '<div class="hash-row"><span class="hash-label">receipt_id</span><span class="hash-val">'
      + escHTML(String(r.receipt_id).substring(0,40)) + '…</span></div>'
      + (r.numbers ? '<div style="font-size:12px;color:var(--text-dim);margin:6px 0">declarations '
          + escHTML(String(r.numbers.declarations)) + ' · axioms ' + escHTML(String(r.numbers.axioms_unique))
          + ' · sorries ' + escHTML(String(r.numbers.sorries_noncomment)) + ' · kernel '
          + escHTML(String(r.kernel_commit_short || '')) + '</div>' : '')
      + '<div style="margin:8px 0">' + honestyHTML + '</div>'
      + '<div style="font-size:12px;color:var(--text-mute)">signing: ' + escHTML(sg.format || '—')
      + (sg.bytes ? ' (' + escHTML(String(sg.bytes)) + ' bytes)' : '') + '</div>'
      + '<div style="margin-top:8px;font-size:12px"><a href="' + hfBase + 'lutar_lean_receipts.ndjson" target="_blank" rel="noopener">Canonical rows on Hugging Face ↗</a>'
      + ' &nbsp;·&nbsp; <a href="https://pypi.org/project/szl-receipt/" target="_blank" rel="noopener">Verify offline (szl-receipt)</a></div></div>';
  });
  ama.forEach(r => {
    cardsHTML += '<div class="formula-card"><div class="formula-card-head">'
      + '<span class="formula-id">amaru</span><span class="formula-name">' + escHTML(r.kind || 'tick') + '</span>'
      + '<span class="chip ' + (r.lambda_pass ? 'chip-ok' : 'chip-err') + '">Λ ' + escHTML(String(r.lambda)) + ' '
      + (r.lambda_pass ? 'PASS' : 'FAIL') + '</span><span class="conj">Conjecture 1 — advisory</span></div>'
      + '<div class="hash-row"><span class="hash-label">receipt_id</span><span class="hash-val">'
      + escHTML(String(r.receipt_id).substring(0,40)) + '…</span></div>'
      + '<div style="font-size:12px;color:var(--text-dim);margin:6px 0">doctrine ' + escHTML(String(r.doctrine))
      + ' · decl ' + escHTML(String(r.decl)) + ' · axioms ' + escHTML(String(r.axioms)) + ' · sorries '
      + escHTML(String(r.sorries)) + ' · anchor ' + escHTML(String(r.lutar_anchor || '')) + '</div>'
      + '<div style="font-size:12px;color:var(--text-mute)">DSSE ' + (r.dsse_signed ? 'signed ✓' : 'unsigned')
      + ' · keyid ' + escHTML(String(r.dsse_keyid || '—')) + '</div>'
      + '<div style="margin-top:8px;font-size:12px"><a href="' + hfBase + 'amaru_receipts.ndjson" target="_blank" rel="noopener">Canonical rows on Hugging Face ↗</a>'
      + ' &nbsp;·&nbsp; <a href="' + escHTML(String(r.verify_key_url || '#')) + '" target="_blank" rel="noopener">Public key ↗</a></div></div>';
  });
  el('ledger-cards').innerHTML = cardsHTML;

  show('ledger-panel');
  setStatus('ledger-status', 'Chain: ' + (intact ? 'INTACT' : 'BROKEN') + ' (' + links + '/' + lut.length
    + ' links) · ' + (lut.length + ama.length) + ' real receipts shown · signatures verify offline against Hugging Face.');
  btn.disabled = false;
}
</script>

</body>
</html>