Spaces:

SZLHOLDINGS
/

a11oy

Running

File size: 26,012 Bytes

234aee9

<!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>