diff --git a/docs/optimistic-accountability.md b/docs/optimistic-accountability.md
index 75647dd..38fee2a 100644
--- a/docs/optimistic-accountability.md
+++ b/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)