essay: bound the rollup analogy to the paper's precise framing

Part II rewritten (doc-only; the attested freeze 172a1d0 is untouched).
The earlier draft claimed the resemblance 'is not a metaphor', called
the extractors fraud proofs 'in the strict sense', and said the system
'cannot fail to convict' — the same compressed overclaims the paper
removed in its round-12 revision. Now: the extractors are REDUCTION
WITNESSES against SHA-256 collision resistance (accepting a forged
consistency proof would break the hash; it does not by itself prove
operator misconduct); the one direct-attribution mechanism is
equivocation evidence (two conflicting signed heads, same size, one log
context — signature layer, not hash layer); a fabricated LEAF is caught
only by off-protocol independent replay. Three disanalogies stated
plainly; the entry-13 closing reframed to the plain fact, no metaphor
needed. Framing note added at top disclosing the correction.

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. |
-| **entry 13** | The next leaf: the attestation of the corpus itself. Does not exist yet. |
+| **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 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)
@@ -80,7 +80,7 @@ NEW_SIZE         = 13
 | log public key | `lean-transparency-log/provider.ed25519.pub` (PEM) | fingerprint `874c8a00…a56a` in `log-metadata.json` |
 | log PRIVATE key | **RESOLVED 2026-07-12**: laptop-side, mode 0600, inside a gitignored state dir of the pacta working tree (exact path in operator-private notes, deliberately not in this public file); public half byte-matches `provider.ed25519.pub`. NOT on the droplet. encrypted SD backup exists (A3b, operator, 2026-07-14) | A3 done; A3b done |
 | producer driver | **RESOLVED 2026-07-12**: it exists and is committed — pacta's `provider/` CLI (`python3 -m pacta_provider`: `check` → signed attestation; `log-append` → leaf + signed STH + receipt; `log-publish` → public face). Heads are signed with `signing_backend: verified-dalek-serial` (the dogfooded verified signer), `self_inclusion: verified`. Only the per-run orchestration was session work | see step A4 (rehearsal, not reconstruction) |
-| server deployment | private repo `PersonalCloudServer` (github, `master`) — since `a186bac` includes the ltl vhost/service/reconstruct.py, md5-verified == droplet | see its `DEPLOY.md` § "The LTL service" |
+| server deployment | the private infrastructure repo (github, `master`) — since `a186bac` includes the ltl vhost/service/reconstruct.py, md5-verified == droplet | see its `DEPLOY.md` § "The LTL service" |
 
 ---
 
@@ -375,7 +375,7 @@ the pin to 13. **Check:** exit 0, pin now 13.
 ### B4. Publish (the single irreversible step)
 The droplet serves the log from a DERIVED dir (`~/cloud/ltl/log`),
 rebuilt from a content mirror (`~/cloud/ltl/published`) — a bare
-`git pull` in `app/` is NOT enough (PersonalCloudServer DEPLOY.md
+`git pull` in `app/` is NOT enough (the private infra repo's DEPLOY.md
 § "The LTL service").
 ```
 cd <log clone> && git add -A && git commit -m "log update: leaf 12 - attestation of ltl-accumulator-verified@$SUBJECT_COMMIT (mechanized-model scope; KNOWN-GAPS 14/15)" && git push origin main
@@ -422,7 +422,7 @@ concrete object, not an unbound assertion).
 - Publish the accumulator blog post: source parked at
   `docs/optimistic-accountability.md` (this repo) — condense to the
   blog's voice, END WITH A LINK TO THE LIVE LEAF (that is why it
-  waited), operator reviews, then one .md into PersonalCloudServer
+  waited), operator reviews, then one .md into the private infra repo
   `blog/posts/`, `build-blog.py`, rsync per its DEPLOY.md. Closes the
   "one post per public repo" gap for this repo.
 - One-line note in this file: date, leaf hash, head root. Commit.

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
-"The Lean Transparency Log" (https://ltl.zkdefi.org/paper): the Merkle
+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
+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"
-(https://ltl.zkdefi.org/paper), §6 and §10 (which scopes the
-mechanization to items i–v).
+This map is the review surface.
 
 | paper item | Lean name | file | cone |
 |---|---|---|---|

docs/optimistic-accountability.md

@@ -1,12 +1,18 @@
 # Optimistic by construction: what the LTL holds, and what it shares with rollups
 
-Status: published. The condensed blog version is live at
-blog.zkdefi.org ("The log notarizes itself — entry 13", 2026-07-16),
-and the closing claim — "the log carries kernel-checked proofs of its
-own machinery" — is now literally true: entry 13 (leaf index 12, hash
-`8cb258d6…`, subject `ltl-accumulator-verified@172a1d0`) is live under
-head `tree size 13, root 3488a2d0…`, verifiable at
-ltl.zkdefi.org/v1/sth. This essay remains the long-form source.
+Status: long-form source. Entry 13 (leaf index 12, hash `8cb258d6…`,
+subject `ltl-accumulator-verified@172a1d0`) is live under head
+`tree size 13, root 3488a2d0…`, verifiable at ltl.zkdefi.org/v1/sth.
+
+Framing note (2026-07-19): Part II was revised to match the precise
+treatment used in the paper. The rollup resemblance is a **bounded
+analogy**, not a strict claim: the collision extractors are *reduction
+witnesses* against SHA-256's collision resistance, not on-protocol
+fraud proofs that convict the operator; a fabricated leaf is caught
+only by *off-protocol* independent replay. Earlier drafts overstated
+this ("fraud proof in the strict sense", "cannot fail to convict"); the
+overstatement is corrected here and the paper omits the analogy from
+its body entirely.
 
 ---
 
@@ -52,70 +58,88 @@ contract is wise; the notary makes it impossible to later dispute
 evident. The LTL is a notary whose every stamped page happens to carry
 instructions for independently re-checking the page's claim.
 
-## Part II — The optimistic-rollup resemblance (it is not a metaphor)
+## Part II — The optimistic-rollup resemblance (a bounded analogy)
 
 Optimistic rollups rest on one bet: *claims are cheap to make and
 expensive to get away with*. A sequencer posts state roots without
-proof; safety comes from anyone's ability to produce a fraud proof
-from public data, and from punishment when they do. The LTL — like its
-direct ancestor, Certificate Transparency (RFC 9162) — is built on the
-same bet: record everything append-only, and make misbehavior generate
-publicly verifiable, transferable evidence.
+proof; safety comes from anyone's ability to produce compact,
+transferable evidence of a specific fault from public data, and from
+punishment when they do. The LTL — like its direct ancestor,
+Certificate Transparency (RFC 9162) — sits at the same design *point*:
+record everything append-only, and make misbehavior produce publicly
+verifiable evidence. The correspondence is a genuine and useful
+analogy, and — this is the part worth getting right — it is an analogy
+with three honest disanalogies, not an equivalence. The precise
+version is what makes it interesting.
 
-The fraud-proof analogue exists in the LTL at two distinct layers:
+There are two very different "faults" a reader tends to conflate, and
+the LTL treats them differently.
 
-**1. Log-layer fraud (operator rewrites or forks history).** Here the
-resemblance is nearly literal, and it is exactly what this corpus
-mechanized. Theorem 3 (`extractCons_correct` / `acceptCons_sound`)
-states: if the verifier accepts a consistency proof between a pinned
-head and a rewritten history, the named extractor **outputs a SHA-256
-collision as two concrete byte strings**. That is a fraud proof in the
-strict sense — and a constructive one: the adversary's own accepted
-messages are compiled into the evidence against them. Equivocation has
-the same shape: two conflicting signed heads ARE the fraud proof, and
-the consumer's pin-store is the watchtower that collects them. Even
-the rollup's liveness assumption transfers: someone must actually
-watch (a pinned consumer, a mirror, a `witness-audit` run). An
-unwatched log, like an unwatched rollup, is safe only on paper.
+**Fault 1 — the operator rewrites or forks the log's own history.**
+This is the layer this corpus mechanized, and it is where the
+resemblance is strongest — but the mechanized result is a *reduction*,
+not a courtroom verdict. Theorem 3 (`extractCons_correct` /
+`acceptCons_sound`) states: if the verifier accepts a consistency proof
+between a pinned head and a rewritten history, the named extractor
+**outputs a SHA-256 collision as two concrete byte strings**. Read that
+statement exactly. It does not say "the operator is guilty"; it says
+"accepting this would break SHA-256." The extractor is a reduction
+witness: it converts a successful attack on the log's structure into a
+concrete refutation of the hash function's collision resistance. Under
+the standing assumption that no such collision is feasible, the attack
+therefore cannot succeed in the first place — which is a *stronger and
+cleaner* guarantee than a fraud proof that convicts after the fact.
+Equivocation is the one place the operator is directly on the hook:
+two conflicting signed heads at the same size, in one log context, are
+transferable evidence attributable to the key holder (this reduces to signature
+unforgeability, not to collision resistance) — the closest analogue to
+a rollup fraud proof against the sequencer, and the consumer's
+pin-store is the watchtower that collects it. The liveness assumption
+transfers cleanly: someone must actually watch (a pinned consumer, a
+mirror, a `witness-audit` run). An unwatched log, like an unwatched
+rollup, is safe only on paper.
 
-**2. Claim-layer fraud (a leaf's content is a lie).** The log does not
-validate Lean proofs on append — it records the claim. That is the
-optimistic part. The fraud proof here is **replay**: the leaf pins
-everything needed to re-run the check, and the failed replay is the
-demonstration. Two properties compare favorably with rollups: the
-challenge window is *infinite* (append-only preserves the crime scene
-forever — a false leaf cannot be reverted, only exposed, and its
-permanence is the exposure), and no adjudicator is needed — the fraud
-proof is reproducible by every reader independently.
+**Fault 2 — a leaf's content is simply false** (the operator lies about
+a Lean result it never actually observed). This is the optimistic part,
+and it is the honest limit of the whole design: the cryptography does
+**not** catch it. The Merkle machinery faithfully commits and orders a
+false statement exactly as it would a true one — it notarizes, it does
+not referee. What catches a false leaf is **independent replay**: the
+leaf pins the commit and toolchain, so anyone can re-run the check, and
+a failed replay is the demonstration. But replay is *off-protocol* —
+it is not a challenge transaction the log adjudicates; it is work a
+third party does with a theorem prover, and the log's only contribution
+is to make the claim precise enough to be replayable and impossible to
+later unsay. Two properties do compare favorably: the challenge window
+is effectively infinite (append-only preserves the record forever — a
+false leaf cannot be reverted, only exposed), and no privileged
+adjudicator exists — every reader replays independently.
 
-**Where the analogy honestly stops: enforcement.** A rollup's fraud
-proof triggers protocol-native consequences — state reverts, bonds are
-slashed, money moves. The LTL has no bond, no slashing, no revert.
-Evidence leads to out-of-band consequences (consumers stop trusting;
-the evidence is publicized), exactly as in CT, where the "slash" is a
-browser distrusting a CA. Same detection architecture, different
-enforcement layer: cryptographic accountability with reputational
-rather than economic stakes. Bolting on economic slashing would
-require on-chain adjudication of "the Lean replay failed" — a
-fraud-proof VM able to run a proof checker; theoretically the same
-construction rollups use, practically a research program. The
-pragmatic dual, implemented in this estate, is consumer-side defense:
-warden's quorum of independently attested verifiers, instead of
-prover-side bonding.
+**The three disanalogies, stated plainly.** (1) The consistency and
+inclusion extractors are reduction witnesses against a cryptographic
+assumption, not on-protocol fraud proofs against the operator — a false
+opening refutes SHA-256, it does not by itself prove misconduct. (2)
+Detecting a fabricated *leaf* requires off-protocol independent replay;
+the log defines no challenge transaction, adjudicator, or compact proof
+that a replay observation was fabricated. (3) There is no bond, no
+slashing, no revert: consequences are reputational and out-of-band —
+consumers stop trusting and the evidence is publicized — exactly as in
+CT, where the "slash" is a browser distrusting a CA. Bolting on
+economic slashing would require an on-chain adjudicator able to run a
+proof checker inside a fault-proof VM; theoretically the same
+construction rollups use, practically a research program. The dual this
+estate actually implements is consumer-side defense: warden's quorum of
+independently attested verifiers, instead of prover-side bonding.
 
-**The inversion worth savoring.** Rollup design treats "optimistic +
-fraud proofs" and "validity proofs" as competing answers for the same
-object. This stack uses both, one inside the other: each leaf's
-*payload* is validity-proven in the strongest available sense (the
-Lean kernel — no optimism, no challenge window), while the *envelope*
-carrying it is optimistic/accountability-style. And entry 13 closes a
-loop that optimistic rollups themselves aspire to and largely lack:
-**formally verified fraud-proof machinery**. The mechanized theorems
-say precisely "this fraud-proof system cannot fail to convict" — any
-accepted rewrite yields the collision, constructively. Production
-rollups would love a kernel-checked proof of their fault-proof
-interpreters; this log carries one for its own — entry 13, inside the
-very ledger it protects.
+**What entry 13 does close.** Set the analogy aside and state the plain
+fact: the log now carries, as one of its own leaves, a kernel-checked
+mechanization of the very soundness arguments its accumulator relies
+on — the extractors, the consistency binding, the per-step pin safety
+— scoped honestly to the recursive model (not the deployed verifier;
+see `KNOWN-GAPS.md`). Whatever one calls that machinery, its proofs are
+now inside the ledger it protects, verifiable end to end by anyone with
+a stock toolchain. That is the loop worth savoring, and it needs no
+rollup metaphor to be remarkable.
 
 ## Pointers (for the eventual blog rendering)