docs: paper-numbering disambiguation + runbook facts updated (doc audit 2026-07-19)

The paper was reinvented (new title, new section/theorem numbering, old
report archived at /paper/v0.2), which made this repo's paper references
ambiguous — worst case: KNOWN-GAPS gap 14/15 cites 'paper §5.3/§5.4'
meaning the OLD report's pin-store sections, while the CURRENT paper's
§5.3/§5.4 are entirely different content. Fixes:
- README: points to the archived v0.2 (the version this corpus was built
  against) AND the current paper (which presents the results in its §5
  and carries this corpus as entry 13).
- STATEMENT-MAP + KNOWN-GAPS: explicit numbering notes — all 'paper §N'
  references are v0.2 numbering; do not match against the current paper.
- ATTESTATION-RUNBOOK facts table: the 'log' row claimed 12 leaves
  FROZEN and the 'entry 13' row claimed 'does not exist yet' — both now
  state execution-time vs current state (13 leaves, 3488a2d0, entry 13
  live; the runbook is the record of that execution).
No Lean, verification, or attestation content touched; the attested
freeze commit 172a1d0 is unaffected (attestation pins the commit, not
the branch).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

ATTESTATION-RUNBOOK.md

@@ -24,8 +24,8 @@ Agent Appendix at the end. Every step ends in a mechanical check.
 | **operator** | The human running the log service (owner of ltl.zkdefi.org and its keys). NOT warden (warden is a consumer). All Phase-B actions are operator actions. |
 | **corpus** | `ltl-accumulator-verified` at freeze commit `172a1d0` (round-5 freeze — the reviewed subject; supersedes the earlier `2da0a79`) — the kernel-checked mechanization of paper §6. |
 | **the button** | `verification/check.sh`. Green means: printed `=== ATTESTATION GREEN (Lean + fidelity) ===` AND `echo $?` printed `0`. BOTH. Never judge from scrolled output. |
-| **the log** | Live service ltl.zkdefi.org + public mirror repo `lean-transparency-log`. Currently 12 leaves (indices 0–11), head root `bcd15f9d…`, FROZEN. |
+| **the log** | Live service ltl.zkdefi.org + public mirror repo `lean-transparency-log`. At execution time: 12 leaves (indices 0–11), head root `bcd15f9d…`, frozen. NOW (post-execution): 13 leaves, head root `3488a2d0…`, entry 13 live. |
-| **entry 13** | The next leaf: the attestation of the corpus itself. Does not exist yet. |
+| **entry 13** | The attestation of the corpus itself. APPENDED 2026-07-16 as leaf index 12 (leaf hash `8cb258d6…`); this runbook is the record of that execution. |
 | **kit round N** | The review package delivered to the external reviewers after freeze N. Round-1 kit = freeze `6e56414`; round 2 = `260ad64`; round 3 = `9972ab4`; round 4 = `2da0a79`; round 5 = `172a1d0`; round 6 = review of `172a1d0` + pacta producer (current). |
 
 ## 2a. Release tuple (the single source of immutable identifiers)

KNOWN-GAPS.md

@@ -1,5 +1,12 @@
 # Known gaps and scope boundaries (honest ledger)
 
+**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
+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.
+
 Deliberate, documented, and none silent. Reviewers should verify this
 list is COMPLETE, not merely that the items are acceptable.
 

README.md

@@ -1,7 +1,11 @@
 # ltl-accumulator-verified
 
-Lean 4 mechanization of the security analysis (§6) of the paper
+Lean 4 mechanization of the security analysis (§6) of the system
-"The Lean Transparency Log" (https://ltl.zkdefi.org/paper): the Merkle
+report "The Lean Transparency Log" (archived at
+https://ltl.zkdefi.org/paper/v0.2 — 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
 accumulator's own correctness and soundness theorems, kernel-checked, in
 the same discipline as the four `*-ed25519-verified` subject corpora.
 
@@ -26,7 +30,8 @@ its own **scope** block: what is kernel-checked is the mechanized model
 KNOWN-GAPS 14/15 — the leaf does not claim the deployed verifier is
 formally verified.
 
-All paper-§6/§10 mechanization targets are kernel-checked; the audit
+All paper-§6/§10 mechanization targets (v0.2 numbering) are
+kernel-checked; the audit
 surface is defined and green (`verification/check.sh`, exit 0). See
 [STATEMENT-MAP.md](STATEMENT-MAP.md) for the paper↔Lean review surface and
 [KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger.

STATEMENT-MAP.md

@@ -1,10 +1,18 @@
 # Statement map: paper §6 ↔ Lean corpus
 
+**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
+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
+results in its §5.1–5.2 under different theorem numbers and cites this
+corpus in its §7.2 coverage table; do not match the numbers below
+against it.
+
 The kernel guarantees every proof below; what a reviewer must vet is the
 **statements** — that each Lean theorem says what the paper's item says.
-This map is the review surface. Paper = "The Lean Transparency Log"
+This map is the review surface.
-(https://ltl.zkdefi.org/paper), §6 and §10 (which scopes the
-mechanization to items i–v).
 
 | paper item | Lean name | file | cone |
 |---|---|---|---|