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

Reusable Dockerfile-COPY-derived deploy from szl-holdings/a11oy main.
Files: 786 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>

pages/verify.html

@@ -297,7 +297,7 @@
 
   <div class="page-hero">
     <h1>Verifiable Inference</h1>
-    <p>Three live demo features. Every receipt is signed and independently verifiable. The honesty is the product.</p>
+    <p>Real, verifiable governance receipts — including our own public ledger. Every receipt is signed and independently verifiable. The honesty is the product.</p>
   </div>
 
   <!-- ===================================================================
@@ -418,6 +418,40 @@
     </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">
@@ -943,6 +977,95 @@ async function loadThesis() {
   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>