def CordialMiners.safePublish {α : Type u_1} [DecidableEq α] (old new : List α) : List α

A safe publish accepts an update only if it extends the current published prefix; otherwise it keeps the current output (the implementation would emit a violation).

Equations

• CordialMiners.safePublish old new = if old <+: new then new else old

theorem CordialMiners.sched_output_prefix_safe {α : Type u_1} [DecidableEq α] (old new : List α) : old <+: safePublish old new

Output-prefix safety (Invariant L.9 / Theorem L.19): a safe publish never regresses, so the stream of published outputs forms a chain under the prefix order and no position is ever rewritten.

theorem CordialMiners.sched_credit_reaches (cost quantum : ℕ) (hq : 0 < quantum) : ∃ (n : ℕ), cost ≤ n * quantum

Bounded-service core (Theorem L.14): with a positive fairness quantum, a continuously runnable wave accrues enough deficit credit to pay for a task of any cost after finitely many scheduler ticks, so it is not starved.