Spaces:
Running
Running
| <!-- 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 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 U</b> is proven but <b>conditional</b> (axiom-free); <b>Λ-uniqueness is | |
| Conjecture 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 U sits above it; | |
| Conjecture 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 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> | |
| ; | |
| /* ============================================================================ | |
| 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 Λ 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 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 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 < 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 = append to back, drain = 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 ≥ 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=>({ "&":"&","<":"<",">":">" }[c])); } | |
| cy.on("tap","node",(e)=>render(e.target.id())); | |
| cy.ready(()=>{ cy.fit(undefined,40); render("thmU"); }); | |
| </script> | |
| </body> | |
| </html> | |