Priority fair-lane progress (the combinatorial core of Theorem K.13): an item enqueued at
position k of a FIFO fair lane reaches the front after k dequeues. With a nonzero fair lane,
every enqueued block is therefore eventually served, so the fair lane does not starve.
theorem
CordialMiners.diss_safety_insert_closed
{P : Type u_1}
{Wave : Type u_2}
{Slot : Type u_3}
{Hash : Type u_4}
[DecidableEq P]
[DecidableEq Wave]
[DecidableEq Slot]
[DecidableEq Hash]
{L : Blocklace P Wave Slot Hash}
{b : Block P Wave Slot Hash}
(hL : ParentClosed L)
(hb : b.parents ⊆ hashesOf L)
:
ParentClosed (insert b L)
DISS safety (Invariant K.1): the receive-path insert of a parent-resolved block preserves parent closure, so dissemination never creates an invalid accepted blocklace.
theorem
CordialMiners.diss_monotone
{P : Type u_1}
{Wave : Type u_2}
{Slot : Type u_3}
{Hash : Type u_4}
[DecidableEq P]
[DecidableEq Wave]
[DecidableEq Slot]
[DecidableEq Hash]
(L : Blocklace P Wave Slot Hash)
(b : Block P Wave Slot Hash)
:
DISS monotonicity (Invariant K.3): without a pruning certificate, the accepted blocklace only grows under dissemination.