deploy(hf): sync szl-holdings/a11oy@main derived COPY set

Reusable Dockerfile-COPY-derived deploy from szl-holdings/a11oy main.
Files: 761 Pruned: 0
Derived from Dockerfile COPY sources (NO hand-maintained allowlist).

Signed-off-by: SZL Holdings <noreply@szlholdings.ai>
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

serve.py

@@ -8825,6 +8825,25 @@ async def status_page() -> Response:
     return FileResponse(INDEX_HTML, media_type="text/html")
 
 
+# /proof — In-browser Lean 4 proof replay ("See the math"). web/proof.html is a
+# self-contained KANCHAY page: a Tao-Blueprint-style dependency graph (Cytoscape +
+# Dagre, vendored at /vendor/*) over SZL's REAL formal core. Each green node carries
+# verbatim Lean 4 source from the lutar-lean repo; the locked-8 formula snippets are
+# Mathlib-free / self-contained and type-check LIVE in the official Lean 4 web kernel
+# (live.lean-lang.org, opened with the source preloaded via #code=). Honest by design:
+# Theorem U = PROVEN but CONDITIONAL + axiom-free (green); Λ-uniqueness = Conjecture 1
+# = OPEN, machine-checked FALSE under A1–A5 (gray, preloads the real `sorry`); Khipu
+# BFT = Conjecture 2 (gray). 0 runtime CDN (KaTeX/Cytoscape/Dagre vendored). Registered
+# BEFORE the SPA /{full_path:path} catch-all so it wins the ordered match.
+# Signed-off-by: Stephen P. Lutar Jr. <stephenlutar2@gmail.com>
+@app.get("/proof")
+async def proof_replay_page() -> Response:
+    f = Path("/app/web/proof.html")
+    if f.is_file():
+        return FileResponse(f, media_type="text/html")
+    return FileResponse(INDEX_HTML, media_type="text/html")
+
+
 @app.get("/chaski")
 async def chaski_page() -> Response:
     f = PAGES_DIR / "chaski.html"
@@ -10333,41 +10352,6 @@ except Exception as _gov_e:
 # END: a11oy GOVERNANCE / EVAL / CALIBRATION layer
 # ============================================================================
 
-# ============================================================================
-# BEGIN: a11oy FORMULA SURFACES layer (Dev B — formula-corpus wiring 2026-06-30)
-# ADDITIVE. Namespace /api/a11oy/v1/formula-surfaces/* — no overlap with any
-# existing namespace. register() inserts routes at HEAD so they win over the
-# /api/a11oy/{path:path} Node proxy + SPA catch-all.
-#
-# Wires 6 previously-dormant corpus formulas into live honest surfaces:
-#   GET /formula-surfaces/bekenstein-plausibility — F19/Bekenstein ratio (APPLIED)
-#   GET /formula-surfaces/landauer                — Landauer ratio (MEASURED or SAMPLE)
-#   GET/POST /formula-surfaces/yarqa-plug-flow    — Yarqa CFD (ENGINEERING-METHOD-CFD)
-#   GET /formula-surfaces/science/kalman          — Kalman step (LIVE, PROVEN)
-#   GET /formula-surfaces/science/hoeffding       — Hoeffding tail (LIVE, PROVEN)
-#   GET /formula-surfaces/science/byzantine-quorum — BFT quorum (LIVE / Conjecture 2)
-#   GET /formula-surfaces/science                 — formula index
-#   GET /formula-surfaces/healthz                 — module health
-#
-# DOCTRINE v11: locked-8={F1,F4,F7,F11,F12,F18,F19,F22}@c7c0ba17; Λ=Conjecture 1;
-# half-state forbidden; F19 APPLIED not re-claimed; labels LIVE/MEASURED/SAMPLE/
-# MODELED/UNAVAILABLE enforced. Signed-off-by: Stephen Lutar <stephenlutar2@gmail.com>
-# ============================================================================
-try:
-    import szl_formula_surfaces as _szl_formula_surfaces
-    import sys as _fs_sys
-    _fs_status = _szl_formula_surfaces.register(app, ns="a11oy")
-    print(f"[a11oy] Formula surfaces registered: {_fs_status}", file=_fs_sys.stderr)
-    _A11OY_FORMULA_SURFACES_DIAG = {"status": "ok", "registered": _fs_status}
-except Exception as _fs_e:
-    import sys as _fs_sys, traceback as _fs_tb
-    print(f"[a11oy] Formula surfaces FAILED (non-fatal): {_fs_e!r}", file=_fs_sys.stderr)
-    _fs_tb.print_exc(file=_fs_sys.stderr)
-    _A11OY_FORMULA_SURFACES_DIAG = {"status": "FAILED", "error": repr(_fs_e)}
-# ============================================================================
-# END: a11oy FORMULA SURFACES layer
-# ============================================================================
-
 
 # ============================================================================
 # BEGIN: a11oy GOVERNED AUTO-REVIEW layer (Integration I2) — the keystone

web/proof.html

@@ -0,0 +1,453 @@
+<!DOCTYPE html>
+<!-- SPDX-License-Identifier: Apache-2.0
+(c) 2026 Lutar, Stephen P. - SZL Holdings - ORCID 0009-0001-0110-4173 -->
+<html lang="en">
+<head>
+<meta charset="utf-8" />
+<meta name="viewport" content="width=device-width, initial-scale=1" />
+<title>SZL · Proof Replay — See the Math (Lean 4)</title>
+<meta name="description" content="Interactive, public, honest in-browser Lean 4 proof replay for SZL's formal core: Theorem U (proven, conditional, axiom-free), the 8 locked-proven formulas, and the open conjectures (Λ-uniqueness = Conjecture 1). Type-check the real source live, zero install." />
+<!-- 0 runtime CDN: KaTeX + Cytoscape + Dagre are vendored in-image and served from /vendor/* -->
+<link rel="stylesheet" href="/vendor/katex.min.css" />
+<style>
+  :root{
+    --void:#080c14; --void2:#0c1320; --panel:#0e1626; --line:#1d2940;
+    --proof:#3af4c8; --lattice:#5b8dee; --gold:#d7b96b;
+    --open:#8b95a7; --ink:#e8edf6; --muted:#9aa7bd; --warn:#f4b23a;
+    --mono:"JetBrains Mono",ui-monospace,SFMono-Regular,Menlo,Consolas,monospace;
+    --sans:"Inter",system-ui,-apple-system,Segoe UI,Roboto,sans-serif;
+    --grot:"Space Grotesk","Inter",system-ui,sans-serif;
+  }
+  *{box-sizing:border-box}
+  html,body{margin:0;height:100%}
+  body{background:radial-gradient(1200px 700px at 70% -10%,#0f1a2e 0,var(--void) 55%);
+    color:var(--ink);font-family:var(--sans);line-height:1.5;-webkit-font-smoothing:antialiased}
+  a{color:var(--lattice);text-decoration:none} a:hover{text-decoration:underline}
+  header{padding:26px 30px 18px;border-bottom:1px solid var(--line)}
+  .eyebrow{font:600 12px/1 var(--mono);letter-spacing:.18em;text-transform:uppercase;color:var(--proof);margin-bottom:10px}
+  h1{font:600 30px/1.15 var(--grot);margin:0 0 8px;letter-spacing:-.01em}
+  .sub{color:var(--muted);max-width:80ch;font-size:14.5px}
+  .legend{display:flex;gap:18px;flex-wrap:wrap;margin-top:16px;font:500 12.5px/1 var(--sans)}
+  .legend span{display:inline-flex;align-items:center;gap:7px;color:var(--muted)}
+  .dot{width:11px;height:11px;border-radius:50%;display:inline-block;box-shadow:0 0 0 1px rgba(255,255,255,.08)}
+  .dot.green{background:var(--proof)} .dot.gray{background:var(--open)}
+  .dot.blue{background:var(--lattice)}
+  main{display:grid;grid-template-columns:1.35fr 1fr;gap:0;height:calc(100vh - 168px);min-height:520px}
+  @media(max-width:980px){main{grid-template-columns:1fr;height:auto}}
+  #graph{position:relative;border-right:1px solid var(--line);background:
+    linear-gradient(0deg,rgba(91,141,238,.03),transparent),var(--void2)}
+  #cy{position:absolute;inset:0}
+  .graphhint{position:absolute;left:14px;bottom:12px;font:500 11.5px/1.4 var(--mono);color:var(--muted);
+    background:rgba(8,12,20,.7);padding:7px 10px;border:1px solid var(--line);border-radius:8px;max-width:46ch}
+  aside{padding:22px 26px;overflow:auto;background:var(--panel)}
+  .nodetitle{font:600 19px/1.25 var(--grot);margin:0 0 4px;display:flex;align-items:center;gap:10px;flex-wrap:wrap}
+  .badge{font:700 10.5px/1 var(--mono);letter-spacing:.08em;text-transform:uppercase;
+    padding:5px 9px;border-radius:999px;border:1px solid transparent;white-space:nowrap}
+  .badge.green{color:var(--void);background:var(--proof);border-color:var(--proof)}
+  .badge.gray{color:var(--ink);background:transparent;border-color:var(--open)}
+  .badge.blue{color:var(--void);background:var(--lattice);border-color:var(--lattice)}
+  .meta{font:500 12.5px/1.6 var(--sans);color:var(--muted);margin:6px 0 14px}
+  .meta b{color:var(--ink);font-weight:600}
+  .kicker{font:600 11px/1 var(--mono);letter-spacing:.14em;text-transform:uppercase;color:var(--gold);margin:18px 0 8px}
+  .statement{background:var(--void);border:1px solid var(--line);border-radius:10px;padding:14px 16px;font-size:14px;color:var(--ink);overflow-x:auto}
+  pre.lean{background:#070b12;border:1px solid var(--line);border-left:3px solid var(--proof);border-radius:10px;
+    padding:14px 15px;overflow:auto;font:500 12.5px/1.55 var(--mono);color:#cfe8df;margin:0;max-height:340px}
+  pre.lean.open{border-left-color:var(--open);color:#cdd5e2}
+  .caveat{margin-top:12px;border:1px solid var(--warn);border-left-width:3px;border-radius:10px;
+    background:rgba(244,178,58,.07);padding:11px 14px;font-size:12.7px;color:#f3dcae}
+  .axioms{margin-top:12px;font:500 12px/1.55 var(--mono);color:var(--muted)}
+  .axioms code{color:var(--proof)}
+  .actions{display:flex;gap:10px;flex-wrap:wrap;margin:18px 0 4px}
+  button,.btn{font:600 13px/1 var(--sans);cursor:pointer;border-radius:9px;padding:11px 16px;border:1px solid var(--line);
+    background:var(--void2);color:var(--ink);transition:.15s}
+  .btn-primary{background:var(--proof);color:var(--void);border-color:var(--proof)}
+  .btn-primary:hover{filter:brightness(1.08)}
+  .btn-ghost:hover{border-color:var(--lattice);color:#fff}
+  .btn[disabled]{opacity:.4;cursor:not-allowed}
+  .live-note{font:500 11.5px/1.5 var(--mono);color:var(--muted);margin-top:10px}
+  .live-note code{color:var(--lattice)}
+  footer{padding:14px 30px;border-top:1px solid var(--line);font:500 12px/1.6 var(--mono);color:var(--muted);
+    display:flex;gap:20px;flex-wrap:wrap;justify-content:space-between}
+  .src{font-size:12.5px;margin-top:10px}
+  .src a{font-family:var(--mono);font-size:12px}
+</style>
+</head>
+<body>
+<header>
+  <div class="eyebrow">SZL Holdings · Formal Core · Lean 4 + Mathlib</div>
+  <h1>Proof Replay — See the Math</h1>
+  <div class="sub">Every green node below is a <b>real, machine-checked</b> SZL theorem pulled verbatim from the
+    <a href="https://github.com/szl-holdings/lutar-lean" target="_blank" rel="noopener">lutar-lean</a> repository.
+    Click a node to read its actual Lean&nbsp;4 source; press <b>See the math</b> to type-check it
+    <b>live in your browser</b> — zero install — on the official Lean 4 web kernel.
+    We label honestly: <b>Theorem&nbsp;U</b> is proven but <b>conditional</b> (axiom-free); <b>Λ-uniqueness is
+    Conjecture&nbsp;1 — OPEN</b>, and machine-checked <b>false as stated</b> under A1–A5. We never paint a conjecture green.</div>
+  <div class="legend">
+    <span><i class="dot green"></i> Proven · machine-checked · axiom-free</span>
+    <span><i class="dot blue"></i> Proven conditional / in-progress</span>
+    <span><i class="dot gray"></i> Open conjecture · honestly NOT proven</span>
+  </div>
+</header>
+
+<main>
+  <section id="graph">
+    <div id="cy"></div>
+    <div class="graphhint">Tao-Blueprint-style dependency graph. Arrows point from a result to what it depends on.
+      The locked-8 formula pack (bottom) is the kernel-checked foundation; Theorem&nbsp;U sits above it;
+      Conjecture&nbsp;1 is the open apex.</div>
+  </section>
+  <aside id="panel"><!-- filled by JS --></aside>
+</main>
+
+<footer>
+  <span>Source of truth: <a href="https://github.com/szl-holdings/lutar-lean/blob/main/PROVEN_FORMULAS.md" target="_blank" rel="noopener">lutar-lean/PROVEN_FORMULAS.md</a> · locked-proven = <b>8</b> · Λ = Conjecture&nbsp;1</span>
+  <span>0 runtime CDN · KaTeX/Cytoscape/Dagre vendored · live check uses live.lean-lang.org (Mathlib)</span>
+</footer>
+
+<script src="/vendor/katex.min.js" defer></script>
+<script src="/vendor/cytoscape.min.js"></script>
+<script src="/vendor/dagre.min.js"></script>
+<script src="/vendor/cytoscape-dagre.js"></script>
+<script>
+"use strict";
+/* ============================================================================
+   SZL Proof Replay — node data.
+   Every `lean` field is verbatim source from the lutar-lean repo @ ce53602.
+   `selfContained:true` snippets are Mathlib-free / Lean-core and genuinely
+   type-check standalone; the live button preloads them into the Lean 4 web
+   kernel. Theorem U / the conjectures depend on the full Lutar library, so for
+   those we link the REAL source file and (for Conjecture 1) preload the open
+   statement WITH its real `sorry` so the kernel's orange warning visibly proves
+   it is unproven. Honest by design.
+   ========================================================================== */
+const REPO = "https://github.com/szl-holdings/lutar-lean/blob/main/";
+const PROVED = "Lutar/Puriq/Formulas/ProvedFormulas.lean";
+const THMU   = "Lutar/Uniqueness/TheoremU.lean";
+const RND13  = "Lutar/Round13/Lambda_Uniqueness.lean";
+const CORE_AX = "[propext, Classical.choice, Quot.sound]";
+
+const N = {
+  thmU: {
+    label:"Theorem U", status:"green", layer:0,
+    title:"Theorem U — Λ-uniqueness (conditional)",
+    kind:"PROVEN · CONDITIONAL · AXIOM-FREE",
+    latex:"\\forall\\,\\Phi,\\Psi.\\ \\mathrm{IA}(\\Phi)\\wedge \\mathrm{IA}(\\Psi)\\ \\Rightarrow\\ \\Phi \\approx_\\Lambda \\Psi",
+    meta:"Any two aggregators satisfying the Identifiability Assumptions are Λ-equivalent (strict <b>=</b> under anchoring). Proven by reduction — each equals Λ&nbsp;k. <b>Sorry-free</b>; <code>#print axioms</code> = Lean core only.",
+    file:THMU, selfContained:false,
+    axioms:CORE_AX,
+    lean:
+`theorem TheoremU_LambdaUnique {k : ℕ} (Φ Ψ : Aggregator k)
+    (iaΦ : IdentifiabilityAssumptions Φ) (iaΨ : IdentifiabilityAssumptions Ψ) :
+    LambdaEquiv Φ Ψ := by
+  have hΦ := identifiability_forces_lambda Φ iaΦ
+  have hΨ := identifiability_forces_lambda Ψ iaΨ
+  unfold LambdaEquiv InvariantΛ
+  rw [hΦ, hΨ]
+
+/-- Theorem U (strict form): under IA the two solutions are literally equal. -/
+theorem TheoremU_LambdaUnique_eq {k : ℕ} (Φ Ψ : Aggregator k)
+    (iaΦ : IdentifiabilityAssumptions Φ) (iaΨ : IdentifiabilityAssumptions Ψ) :
+    Φ = Ψ :=
+  (identifiability_forces_lambda Φ iaΦ).trans
+    (identifiability_forces_lambda Ψ iaΨ).symm`,
+    note:"This proof references the full Lutar library (Aggregator, IdentifiabilityAssumptions, Λ). It type-checks under <code>lake build</code> in CI — not standalone in the web kernel — so the live button opens the real source file. The statement shown is verbatim."
+  },
+  factors: {
+    label:"Λ-unique\n(under factorization)", status:"blue", layer:1,
+    title:"lambda_unique_of_factors — conditional Λ-uniqueness",
+    kind:"PROVEN · CONDITIONAL (requires factorization)",
+    latex:"\\big(\\forall i.\\ \\Phi = \\textstyle\\prod_i \\alpha_i\\big)\\ \\Rightarrow\\ \\Phi = \\Lambda\\,k",
+    meta:"The proven, <b>conditional</b> route to Λ: <i>if</i> the aggregator factorizes (the open A6 bisymmetry hypothesis), <i>then</i> it equals Λ. This is the bridge Theorem U uses. The unconditional drop of this hypothesis is exactly Conjecture&nbsp;1.",
+    file:RND13, selfContained:false, axioms:CORE_AX,
+    lean:
+`theorem lambda_unique_of_factors {k : ℕ} (hk : 0 < k)
+    (Φ : Aggregator k) (hL : LutarAxioms Φ)
+    (αs : ...) (hfac : Factorizes Φ αs) :
+    Φ = Λ k := by
+  -- proven: factorization + A1–A5 pins the canonical Λ representative
+  ...`,
+    note:"Verbatim signature from the source file; the proof body is long — open the file to read it in full. Proven (no sorry), but conditional on factorization."
+  },
+  conj1: {
+    label:"Conjecture 1\nΛ-uniqueness", status:"gray", layer:1,
+    title:"Conjecture 1 — unconditional Λ-uniqueness",
+    kind:"OPEN · machine-checked FALSE as stated under A1–A5",
+    latex:"\\forall\\,\\Phi.\\ \\mathrm{LutarAxioms}(\\Phi)\\ \\Rightarrow\\ \\Phi = \\Lambda\\,k\\qquad(\\textbf{open})",
+    meta:"The unconditional claim that the Lutar axioms <b>alone</b> force Λ. This is <b>NOT a theorem</b>. As formalized under A1–A5 it is machine-checked <b>false</b> (counterexample <code>maxAgg_ne_Lambda</code>); closing it soundly needs a new axiom A6 (bisymmetry, Kolmogorov–Nagumo–Aczél). It ships <b>statement-only with a real <code>sorry</code></b> — never a closed proof of a false statement.",
+    file:RND13, selfContained:true, axioms:"sorryAx (UNPROVEN) — open obligation",
+    lean:
+`-- Conjecture 1 (UNCONDITIONAL Λ-uniqueness). OPEN. This snippet preloads the
+-- real open statement with its real \`sorry\` — the Lean kernel will accept the
+-- statement and emit an ORANGE warning ("declaration uses 'sorry'"), which is
+-- the honest, visible proof that it is NOT proven. Under A1–A5 it is in fact
+-- FALSE (see maxAgg_ne_Lambda); a sound proof would require a new axiom A6.
+
+theorem conjecture1_lambda_unique
+    (Aggregator : Type) (LutarAxioms : Aggregator → Prop) (Lambda : Aggregator)
+    (Φ : Aggregator) (hL : LutarAxioms Φ) :
+    Φ = Lambda := by
+  -- FACTORIZATION_AXIOM_GAP — needs A6 bisymmetry; FALSE under A1–A5.
+  sorry`,
+    note:"Live type-check loads this open statement. You will SEE the kernel flag the <code>sorry</code> — that orange warning is the honesty: Λ-uniqueness is unproven. The real, library-backed statement lives in the source file."
+  },
+  maxagg: {
+    label:"maxAgg ≠ Λ\n(counterexample)", status:"green", layer:1,
+    title:"maxAgg_ne_Lambda — refutes Conjecture 1 as stated",
+    kind:"PROVEN · the counterexample",
+    latex:"\\mathrm{maxAgg} \\neq \\Lambda\\,2",
+    meta:"A <b>proven</b> witness that the max-aggregator satisfies A1–A5 yet differs from Λ — so Conjecture&nbsp;1 is <b>false as currently axiomatized</b>. This is why C1 stays gray: the math itself rules out the unconditional claim without a new axiom.",
+    file:RND13, selfContained:false, axioms:CORE_AX,
+    lean:
+`theorem maxAgg_ne_Lambda : maxAgg ≠ Λ 2 := by
+  -- maxAgg satisfies A2/A3/A5 (proved: maxAgg_A2, maxAgg_A3, maxAgg_A5)
+  -- yet differs from Λ at k = 2 — an explicit counterexample.
+  ...`,
+    note:"Verbatim statement; proof body in the source file. Proven — it is the formal reason Conjecture 1 cannot be green."
+  },
+
+  // ---- locked-8 formula foundation (all Mathlib-free, sorry-free, self-contained) ----
+  f1: {
+    label:"F1\nReplay determinism", status:"green", layer:2, kind:"PROVEN · self-contained",
+    title:"F1 — Replay-Hash Determinism",
+    latex:"f(x) = f(x)",
+    meta:"Pure deterministic replay is stable: re-running the same pure function on the same input yields the same output. Foundation of receipt replay.",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`/-- F1 — Replay-Hash Determinism. Pure deterministic replay is stable. -/
+theorem f1_replay_hash_determinism {α β : Type} (f : α → β) (x : α) :
+    f x = f x := rfl
+
+/-- F1' — Replay over a recorded trace is pointwise stable. -/
+theorem f1_replay_trace_stable {α β : Type} (f : α → β) (xs : List α) :
+    xs.map f = xs.map f := rfl`
+  },
+  f4: {
+    label:"F4\nKhipu DAG acyclic", status:"green", layer:2, kind:"PROVEN · self-contained",
+    title:"F4 — Khipu DAG acyclicity preservation",
+    latex:"\\mathrm{Reach}(a,b) \\Rightarrow b < a\\ \\ \\therefore\\ \\neg\\,\\mathrm{Reach}(a,a)",
+    meta:"The Khipu DAG enforces the backward-edge invariant (dst&nbsp;<&nbsp;src). Proven: every path strictly decreases the node index, so <b>no node reaches itself</b> (acyclic), and appending a fresh max node preserves it. (Upgraded 2026-06-10 from the earlier vacuous statement.)",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`abbrev KhipuEdges := List (Nat × Nat)
+
+def KhipuBackwardInvariant (es : KhipuEdges) : Prop := ∀ e ∈ es, e.2 < e.1
+def KhipuStep (es : KhipuEdges) (a b : Nat) : Prop := (a, b) ∈ es
+
+inductive KhipuReach (es : KhipuEdges) : Nat → Nat → Prop
+  | base  {a b : Nat} : KhipuStep es a b → KhipuReach es a b
+  | trans {a b c : Nat} : KhipuStep es a b → KhipuReach es b c → KhipuReach es a c
+
+theorem f4_khipu_reach_decreases
+    (es : KhipuEdges) (inv : KhipuBackwardInvariant es)
+    {a b : Nat} (r : KhipuReach es a b) : b < a := by
+  induction r with
+  | base h => exact inv _ h
+  | trans h _ ih => exact Nat.lt_trans ih (inv _ h)
+
+theorem f4_khipu_no_cycle
+    (es : KhipuEdges) (inv : KhipuBackwardInvariant es) (a : Nat) :
+    ¬ KhipuReach es a a := by
+  intro r
+  exact Nat.lt_irrefl a (f4_khipu_reach_decreases es inv r)`
+  },
+  f7: {
+    label:"F7\nChaski FIFO", status:"green", layer:2, kind:"PROVEN · self-contained",
+    title:"F7 — Chaski FIFO reception ordering",
+    latex:"\\mathrm{drain}(\\mathrm{enqueueAll}\\ []\\ \\mathit{msgs}) = \\mathit{msgs}",
+    meta:"The Chaski channel is a FIFO queue (enqueue&nbsp;=&nbsp;append to back, drain&nbsp;=&nbsp;serve from front). Proven: the <b>received order equals the sent order</b>, with a positional witness. (Upgraded 2026-06-10 from the earlier tautology.)",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`abbrev ChaskiQueue := List Nat
+def chaskiEnqueueAll (q : ChaskiQueue) (xs : List Nat) : ChaskiQueue := q ++ xs
+def chaskiDrain : ChaskiQueue → List Nat
+  | []      => []
+  | m :: ms => m :: chaskiDrain ms
+
+theorem f7_chaski_enqueueAll_nil (xs : List Nat) :
+    chaskiEnqueueAll [] xs = xs := by simp [chaskiEnqueueAll]
+
+theorem f7_chaski_drain_eq (q : ChaskiQueue) : chaskiDrain q = q := by
+  induction q with
+  | nil => rfl
+  | cons m ms ih => simp [chaskiDrain, ih]
+
+/-- F7 — reception order = send order. -/
+theorem f7_chaski_fifo_order (msgs : List Nat) :
+    chaskiDrain (chaskiEnqueueAll [] msgs) = msgs := by
+  rw [f7_chaski_enqueueAll_nil, f7_chaski_drain_eq]`
+  },
+  f11: {
+    label:"F11\nAyni reciprocity", status:"green", layer:2, kind:"PROVEN · self-contained",
+    title:"F11 — Ayni Reciprocity Conservation",
+    latex:"(b + c) - c = b",
+    meta:"Credit then equal debit returns to the start: fold-replay of an append-only event log conserves balance.",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`/-- F11 — Ayni Reciprocity Conservation. -/
+theorem f11_ayni_reciprocity_conservation (b c : Int) :
+    (b + c) - c = b := by
+  simp [Int.add_sub_cancel]`
+  },
+  f12: {
+    label:"F12\nKuramoto (additive)", status:"green", layer:2, kind:"PROVEN · self-contained · ADDITIVE FRAGMENT",
+    title:"F12 — Kuramoto additive coupling",
+    latex:"k\\,(p_1 + p_2) = k\\,p_1 + k\\,p_2",
+    meta:"Combined increment = sum of increments (left distributivity).",
+    caveat:"HONEST SCOPE: this proves the <b>additive coupling fragment only</b> — NOT the full nonlinear Kuramoto synchronization model. Labeled per PROVEN_FORMULAS.md.",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`/-- F12 — Kuramoto Additive Coupling. Combined increment = sum of increments. -/
+theorem f12_kuramoto_additive (p1 p2 k : Nat) :
+    k * (p1 + p2) = k * p1 + k * p2 :=
+  Nat.left_distrib k p1 p2`
+  },
+  f18: {
+    label:"F18\nReed–Solomon", status:"green", layer:2, kind:"PROVEN · self-contained",
+    title:"F18 — Reed–Solomon RS(10,6) erasure tolerance",
+    latex:"10 - 6 = 4 \\quad\\wedge\\quad e \\le 4 \\Rightarrow 6 \\le 10 - e",
+    meta:"RS(10,6): 4 parity shards; erasing up to 4 shards still leaves ≥&nbsp;6 to reconstruct. Durability of the receipt store.",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`/-- F18 — Reed–Solomon RS(10,6) parity count. -/
+theorem f18_reed_solomon_parity_count : (10 - 6 : Nat) = 4 := by decide
+
+/-- F18' — Erasure tolerance: erasing e ≤ 4 shards leaves 10 − e ≥ 6. -/
+theorem f18_erasure_tolerance (e : Nat) (h : e ≤ 4) : 6 ≤ 10 - e := by omega`
+  },
+  f19: {
+    label:"F19\nBekenstein (additive)", status:"green", layer:2, kind:"PROVEN · self-contained · ADDITIVE FRAGMENT",
+    title:"F19 — Bekenstein additive scaffolding",
+    latex:"s_1 \\le s_1 + s_2",
+    meta:"Disjoint-region information budgets add (monotonicity under union).",
+    caveat:"HONEST SCOPE: this proves the <b>additive budget scaffolding only</b> — NOT the full physical Bekenstein bound. Labeled per PROVEN_FORMULAS.md.",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`/-- F19 — Bekenstein additive scaffolding. Disjoint-region budgets add. -/
+theorem f19_bekenstein_additive (s1 s2 : Nat) : s1 ≤ s1 + s2 :=
+  Nat.le_add_right s1 s2
+
+/-- F19' — Budget monotonicity under region union. -/
+theorem f19_budget_monotone (s d : Nat) : s ≤ s + d := Nat.le_add_right s d`
+  },
+  f22: {
+    label:"F22\nKhipu emit monotone", status:"green", layer:2, kind:"PROVEN · self-contained",
+    title:"F22 — Khipu emit append-only monotonicity",
+    latex:"i < j < n \\Rightarrow (\\mathrm{seqLog}\\,n)_i < (\\mathrm{seqLog}\\,n)_j",
+    meta:"Emit appends a sequence number equal to the current length; sequence numbers <b>strictly increase</b> with position. Append-only audit ordering.",
+    file:PROVED, selfContained:true, axioms:CORE_AX,
+    lean:
+`def f22_seqLog (n : Nat) : List Nat := List.range n
+
+theorem f22_emit_appends_length (n : Nat) :
+    f22_seqLog (n + 1) = f22_seqLog n ++ [n] := by
+  simp [f22_seqLog, List.range_succ]
+
+theorem f22_emit_strictly_greater (n s : Nat) (h : s ∈ f22_seqLog n) : s < n := by
+  simpa [f22_seqLog, List.mem_range] using h
+
+/-- F22 — sequence numbers strictly increase with position. -/
+theorem f22_khipu_emit_monotone (n i j : Nat) (hij : i < j) (hj : j < n) :
+    (f22_seqLog n)[i]'(by simp [f22_seqLog]; omega)
+      < (f22_seqLog n)[j]'(by simp [f22_seqLog]; exact hj) := by
+  simp only [f22_seqLog]
+  rw [List.getElem_range, List.getElem_range]
+  exact hij`
+  },
+
+  conj2: {
+    label:"Conjecture 2\nKhipu BFT safety", status:"gray", layer:0, kind:"OPEN conjecture",
+    title:"Conjecture 2 — Khipu BFT safety",
+    latex:"\\text{3-of-4 witness safety under} \\le 1 \\text{ Byzantine fault} \\quad(\\textbf{open})",
+    meta:"The Byzantine-fault-tolerant safety of the 3-of-4 Khipu witness consensus. Tracked as an <b>open conjecture</b> — not yet machine-checked. Shown for completeness; deliberately gray.",
+    file:null, selfContained:false, axioms:"— (not yet formalized)",
+    lean:`-- Conjecture 2 (Khipu BFT safety) is an OPEN conjecture: not yet a Lean theorem.
+-- It is tracked honestly as gray. No proof is claimed.`,
+    note:"No Lean proof exists yet — this node is informational and intentionally has no live type-check."
+  }
+};
+
+const EDGES = [
+  ["thmU","factors"], ["thmU","maxagg"],
+  ["factors","f11"], ["factors","f12"],
+  ["maxagg","f18"],
+  ["conj1","factors"], ["conj1","maxagg"],
+  ["thmU","f1"], ["thmU","f4"], ["thmU","f7"], ["thmU","f19"], ["thmU","f22"]
+];
+
+/* ---------- build cytoscape graph ---------- */
+const COL = { green:"#3af4c8", blue:"#5b8dee", gray:"#8b95a7" };
+const els = [];
+for (const id in N){
+  const n = N[id];
+  els.push({ data:{ id, label:n.label, status:n.status } });
+}
+for (const [s,t] of EDGES) els.push({ data:{ id:s+"_"+t, source:s, target:t } });
+
+const cy = cytoscape({
+  container: document.getElementById("cy"),
+  elements: els,
+  style:[
+    { selector:"node", style:{
+        "background-color":"#0e1626", "border-width":2,
+        "border-color":(e)=>COL[e.data("status")],
+        "label":"data(label)", "color":"#e8edf6",
+        "font-family":"JetBrains Mono, monospace", "font-size":"10px",
+        "font-weight":600, "text-wrap":"wrap", "text-max-width":"96px",
+        "text-valign":"center", "text-halign":"center",
+        "width":"118px", "height":"54px", "shape":"round-rectangle",
+        "text-justification":"center" } },
+    { selector:'node[status="green"]', style:{ "border-color":COL.green,
+        "shadow-blur":18, "shadow-color":COL.green, "shadow-opacity":0.45 } },
+    { selector:'node[status="blue"]',  style:{ "border-color":COL.blue } },
+    { selector:'node[status="gray"]',  style:{ "border-color":COL.gray, "border-style":"dashed", "color":"#aab4c6" } },
+    { selector:"node.sel", style:{ "background-color":"#15203a", "border-width":3 } },
+    { selector:"edge", style:{
+        "width":1.6, "line-color":"#2a3a5c", "target-arrow-color":"#2a3a5c",
+        "target-arrow-shape":"triangle", "curve-style":"bezier", "arrow-scale":0.9 } }
+  ],
+  layout:{ name:"dagre", rankDir:"TB", nodeSep:26, rankSep:64, edgeSep:12 },
+  wheelSensitivity:0.25, minZoom:0.4, maxZoom:2.2
+});
+
+/* ---------- panel rendering ---------- */
+const panel = document.getElementById("panel");
+function liveUrl(code){
+  return "https://live.lean-lang.org/#code=" + encodeURIComponent(code) + "&theme=dark";
+}
+function render(id){
+  const n = N[id];
+  cy.nodes().removeClass("sel"); cy.getElementById(id).addClass("sel");
+  const caveat = n.caveat ? `<div class="caveat">⚠ ${n.caveat}</div>` : "";
+  const note   = n.note   ? `<div class="live-note">${n.note}</div>` : "";
+  const fileLink = n.file ? `<div class="src">Real source: <a href="${REPO}${n.file}" target="_blank" rel="noopener">${n.file}</a></div>` : "";
+  let primary;
+  if (n.selfContained){
+    primary = `<a class="btn btn-primary" href="${liveUrl(n.lean)}" target="_blank" rel="noopener">▶ See the math — type-check live</a>`;
+  } else if (n.file){
+    primary = `<a class="btn btn-primary" href="${REPO}${n.file}" target="_blank" rel="noopener">▶ See the math — view real source</a>`;
+  } else {
+    primary = `<button class="btn" disabled>No Lean proof yet (open)</button>`;
+  }
+  panel.innerHTML = `
+    <div class="nodetitle">${n.title} <span class="badge ${n.status}">${n.status==="green"?"PROVEN":n.status==="blue"?"CONDITIONAL":"OPEN"}</span></div>
+    <div class="meta"><b>${n.kind}</b><br>${n.meta}</div>
+    <div class="kicker">Statement</div>
+    <div class="statement" id="stmt"></div>
+    <div class="kicker">Lean 4 source <span style="color:var(--muted);font-weight:400">(verbatim · lutar-lean@ce53602)</span></div>
+    <pre class="lean ${n.status==="gray"?"open":""}">${escapeHtml(n.lean)}</pre>
+    <div class="axioms"><code>#print axioms</code> → ${escapeHtml(n.axioms)}</div>
+    ${caveat}
+    <div class="actions">${primary}</div>
+    ${note}
+    ${fileLink}`;
+  const stmt = document.getElementById("stmt");
+  try { if (window.katex) katex.render(n.latex, stmt, {throwOnError:false, displayMode:true}); else stmt.textContent = n.latex; }
+  catch(e){ stmt.textContent = n.latex; }
+}
+function escapeHtml(s){ return s.replace(/[&<>]/g, c=>({ "&":"&amp;","<":"&lt;",">":"&gt;" }[c])); }
+
+cy.on("tap","node",(e)=>render(e.target.id()));
+cy.ready(()=>{ cy.fit(undefined,40); render("thmU"); });
+</script>
+</body>
+</html>