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>

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
+Status: long-form source. Entry 13 (leaf index 12, hash `8cb258d6…`,
-blog.zkdefi.org ("The log notarizes itself — entry 13", 2026-07-16),
+subject `ltl-accumulator-verified@172a1d0`) is live under head
-and the closing claim — "the log carries kernel-checked proofs of its
+`tree size 13, root 3488a2d0…`, verifiable at ltl.zkdefi.org/v1/sth.
-own machinery" — is now literally true: entry 13 (leaf index 12, hash
+
-`8cb258d6…`, subject `ltl-accumulator-verified@172a1d0`) is live under
+Framing note (2026-07-19): Part II was revised to match the precise
-head `tree size 13, root 3488a2d0…`, verifiable at
+treatment used in the paper. The rollup resemblance is a **bounded
-ltl.zkdefi.org/v1/sth. This essay remains the long-form source.
+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
+proof; safety comes from anyone's ability to produce compact,
-from public data, and from punishment when they do. The LTL — like its
+transferable evidence of a specific fault from public data, and from
-direct ancestor, Certificate Transparency (RFC 9162) — is built on the
+punishment when they do. The LTL — like its direct ancestor,
-same bet: record everything append-only, and make misbehavior generate
+Certificate Transparency (RFC 9162) — sits at the same design *point*:
-publicly verifiable, transferable evidence.
+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
+**Fault 1 — the operator rewrites or forks the log's own history.**
-resemblance is nearly literal, and it is exactly what this corpus
+This is the layer this corpus mechanized, and it is where the
-mechanized. Theorem 3 (`extractCons_correct` / `acceptCons_sound`)
+resemblance is strongest — but the mechanized result is a *reduction*,
-states: if the verifier accepts a consistency proof between a pinned
+not a courtroom verdict. Theorem 3 (`extractCons_correct` /
-head and a rewritten history, the named extractor **outputs a SHA-256
+`acceptCons_sound`) states: if the verifier accepts a consistency proof
-collision as two concrete byte strings**. That is a fraud proof in the
+between a pinned head and a rewritten history, the named extractor
-strict sense — and a constructive one: the adversary's own accepted
+**outputs a SHA-256 collision as two concrete byte strings**. Read that
-messages are compiled into the evidence against them. Equivocation has
+statement exactly. It does not say "the operator is guilty"; it says
-the same shape: two conflicting signed heads ARE the fraud proof, and
+"accepting this would break SHA-256." The extractor is a reduction
-the consumer's pin-store is the watchtower that collects them. Even
+witness: it converts a successful attack on the log's structure into a
-the rollup's liveness assumption transfers: someone must actually
+concrete refutation of the hash function's collision resistance. Under
-watch (a pinned consumer, a mirror, a `witness-audit` run). An
+the standing assumption that no such collision is feasible, the attack
-unwatched log, like an unwatched rollup, is safe only on paper.
+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
+**Fault 2 — a leaf's content is simply false** (the operator lies about
-validate Lean proofs on append — it records the claim. That is the
+a Lean result it never actually observed). This is the optimistic part,
-optimistic part. The fraud proof here is **replay**: the leaf pins
+and it is the honest limit of the whole design: the cryptography does
-everything needed to re-run the check, and the failed replay is the
+**not** catch it. The Merkle machinery faithfully commits and orders a
-demonstration. Two properties compare favorably with rollups: the
+false statement exactly as it would a true one — it notarizes, it does
-challenge window is *infinite* (append-only preserves the crime scene
+not referee. What catches a false leaf is **independent replay**: the
-forever — a false leaf cannot be reverted, only exposed, and its
+leaf pins the commit and toolchain, so anyone can re-run the check, and
-permanence is the exposure), and no adjudicator is needed — the fraud
+a failed replay is the demonstration. But replay is *off-protocol* —
-proof is reproducible by every reader independently.
+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
+**The three disanalogies, stated plainly.** (1) The consistency and
-proof triggers protocol-native consequences — state reverts, bonds are
+inclusion extractors are reduction witnesses against a cryptographic
-slashed, money moves. The LTL has no bond, no slashing, no revert.
+assumption, not on-protocol fraud proofs against the operator — a false
-Evidence leads to out-of-band consequences (consumers stop trusting;
+opening refutes SHA-256, it does not by itself prove misconduct. (2)
-the evidence is publicized), exactly as in CT, where the "slash" is a
+Detecting a fabricated *leaf* requires off-protocol independent replay;
-browser distrusting a CA. Same detection architecture, different
+the log defines no challenge transaction, adjudicator, or compact proof
-enforcement layer: cryptographic accountability with reputational
+that a replay observation was fabricated. (3) There is no bond, no
-rather than economic stakes. Bolting on economic slashing would
+slashing, no revert: consequences are reputational and out-of-band —
-require on-chain adjudication of "the Lean replay failed" — a
+consumers stop trusting and the evidence is publicized — exactly as in
-fraud-proof VM able to run a proof checker; theoretically the same
+CT, where the "slash" is a browser distrusting a CA. Bolting on
-construction rollups use, practically a research program. The
+economic slashing would require an on-chain adjudicator able to run a
-pragmatic dual, implemented in this estate, is consumer-side defense:
+proof checker inside a fault-proof VM; theoretically the same
-warden's quorum of independently attested verifiers, instead of
+construction rollups use, practically a research program. The dual this
-prover-side bonding.
+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 +
+**What entry 13 does close.** Set the analogy aside and state the plain
-fraud proofs" and "validity proofs" as competing answers for the same
+fact: the log now carries, as one of its own leaves, a kernel-checked
-object. This stack uses both, one inside the other: each leaf's
+mechanization of the very soundness arguments its accumulator relies
-*payload* is validity-proven in the strongest available sense (the
+on — the extractors, the consistency binding, the per-step pin safety
-Lean kernel — no optimism, no challenge window), while the *envelope*
+— scoped honestly to the recursive model (not the deployed verifier;
-carrying it is optimistic/accountability-style. And entry 13 closes a
+see `KNOWN-GAPS.md`). Whatever one calls that machinery, its proofs are
-loop that optimistic rollups themselves aspire to and largely lack:
+now inside the ledger it protects, verifiable end to end by anyone with
-**formally verified fraud-proof machinery**. The mechanized theorems
+a stock toolchain. That is the loop worth savoring, and it needs no
-say precisely "this fraud-proof system cannot fail to convict" — any
+rollup metaphor to be remarkable.
-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.
 
 ## Pointers (for the eventual blog rendering)