def CordialMiners.leaderList {Hash : Type u_1} (leaderOf : ℕ → Hash) : ℕ → List Hash

The cumulative leader list: the first k canonical leaders, in wave order.

Equations

• CordialMiners.leaderList leaderOf 0 = []
• CordialMiners.leaderList leaderOf k.succ = CordialMiners.leaderList leaderOf k ++ [leaderOf k]

theorem CordialMiners.leaderList_prefix_of_le {Hash : Type u_1} (leaderOf : ℕ → Hash) {m n : ℕ} : m ≤ n → leaderList leaderOf m <+: leaderList leaderOf n

The cumulative leader list is prefix-monotone in its length: more finalized waves give a longer list that extends the shorter one, never reordering it.

def CordialMiners.finalizedAnchors {P : Type u_2} {Wave : Type u_3} {Slot : Type u_4} {Hash : Type u_5} (finalCount : Blocklace P Wave Slot Hash → ℕ) (leaderOf : ℕ → Hash) : Blocklace P Wave Slot Hash → List Hash

The finalized-anchor sequence: the first finalCount L canonical leaders, where finalCount L is the number of consecutively finalized waves in L.

Equations

• CordialMiners.finalizedAnchors finalCount leaderOf L = CordialMiners.leaderList leaderOf (finalCount L)

theorem CordialMiners.finalizedAnchors_prefixMonotone {P : Type u_2} {Wave : Type u_3} {Slot : Type u_4} {Hash : Type u_5} (finalCount : Blocklace P Wave Slot Hash → ℕ) (leaderOf : ℕ → Hash) (hcount : ∀ {L₁ L₂ : Blocklace P Wave Slot Hash}, L₁ ⊆ L₂ → finalCount L₁ ≤ finalCount L₂) : AnchorPrefixMonotone (finalizedAnchors finalCount leaderOf)

Leader safety derived: if the finalized-wave count is monotone in the blocklace (finality permanence plus wave-ordered finalization), the anchor sequence is prefix-monotone. This reduces the leader-safety hypothesis to one scalar fact.