Parked blog-post source, publishes after entry 13 (so it can end with
a live leaf link). Part I: the tree holds verification-event records
(operator claims that name their own evidence via commit+toolchain
pins), not the Lean proofs; three-layer guarantee table (kernel /
replay pin / accumulator). Part II: the optimistic-rollup resemblance
made precise — two fraud layers (log-layer: Theorem 3 as a
constructive fraud-proof generator; claim-layer: replay with an
infinite challenge window), the honest enforcement gap (reputational
vs economic slashing, CT lineage), the watcher/liveness assumption,
and the inversion (validity-proven payload in an optimistic envelope;
entry 13 = formally verified fraud-proof machinery).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>