From 2f284c93a5ff21108f0e283b38816b6d36da0ee2 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 22 Aug 2026 18:43:06 +0200 Subject: [PATCH] coherence sweep: no private paths in public docs; dead /paper/v0.2 links repointed to git history; leaf-index numbering (doc-only) --- KNOWN-GAPS.md | 2 +- README.md | 6 +++--- STATEMENT-MAP.md | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/KNOWN-GAPS.md b/KNOWN-GAPS.md index a4b49dd..f83404d 100644 --- a/KNOWN-GAPS.md +++ b/KNOWN-GAPS.md @@ -2,7 +2,7 @@ **Numbering note (2026-07-19):** "paper §N" references in this ledger use the archived system report's numbering ("The Lean Transparency -Log", https://ltl.zkdefi.org/paper/v0.2), which this corpus was built +Log", the v0.2 draft archived in the pacta repository's git history), which this corpus was built against. The current paper at /paper has a different structure; in particular its §5.3/§5.4 are unrelated to the §5.3/§5.4 cited in gap 14/15 below. diff --git a/README.md b/README.md index af9cc6d..7e56b31 100644 --- a/README.md +++ b/README.md @@ -2,17 +2,17 @@ Lean 4 mechanization of the security analysis (§6) of the system report "The Lean Transparency Log" (archived at -https://ltl.zkdefi.org/paper/v0.2 — the version this corpus was built +the v0.2 draft (archived in the pacta repository's git history) — the version this corpus was built against; the current paper, "Accountable Distribution of Machine-Checked Correctness Evidence" at https://ltl.zkdefi.org/paper, presents these -results in its §5 and carries this corpus as entry 13): the Merkle +results in its §5 and carries this corpus as leaf 12, the log's thirteenth entry): the Merkle accumulator's own correctness and soundness theorems, kernel-checked, in the same discipline as the four `*-ed25519-verified` subject corpora. ## Status: **ATTESTED — LTL leaf 12 (the log's thirteenth entry), 2026-07-16; hardened model re-attested as leaf 17 (2026-08-08)** This corpus is now itself a leaf of the log it describes. It was appended -as **entry 13** of the Lean Transparency Log (freeze `172a1d0`), so the +as **leaf 12** of the Lean Transparency Log (freeze `172a1d0`), so the log carries kernel-checked proofs *about the accumulator model* underlying its own inclusion and consistency reasoning (a deployment we are unaware of a precedent for; scoped to the mechanized model, not the diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md index 34fecf2..dd4a536 100644 --- a/STATEMENT-MAP.md +++ b/STATEMENT-MAP.md @@ -2,7 +2,7 @@ **Numbering note (2026-07-19):** every paper reference in this map uses the numbering of the archived system report — "The Lean Transparency -Log", https://ltl.zkdefi.org/paper/v0.2 — whose §6 this corpus +Log", the v0.2 draft (archived in the pacta repository's git history) — whose §6 this corpus mechanized verbatim and whose §10 scopes the mechanization to items i–v. The current paper ("Accountable Distribution of Machine-Checked Correctness Evidence", https://ltl.zkdefi.org/paper) presents the same