zeekay 4b532ed805 proof: caught-up by acceptance not store presence (LP-304 layer 8) ...

Add the store-presence-fixed-point theorem (a node holding gossiped-but-unaccepted
blocks reports caught-up at its stale height forever), the acceptance-converges
theorem (cert-gated accept of held blocks reaches the frontier), and the
frozen-cache lemma (recognition must read the advancing finalised ledger, not the
plugin LastAccepted cache). Proven on mainnet luxd-2 (1082780 -> 1082796).

2026-06-27 15:47:09 -07:00

243 KiB

Raw Permalink History

View Raw