theorem CordialMiners.findGreatest_mono_pred {P Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (k : ℕ), P k → Q k) (n : ℕ) : Nat.findGreatest P n ≤ Nat.findGreatest Q n

findGreatest is monotone in the predicate: a weaker predicate has a greater (or equal) maximum.

def CordialMiners.finalCountOf {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (Final : Blocklace P Wave Slot Hash → ℕ → Prop) [(L : Blocklace P Wave Slot Hash) → (w : ℕ) → Decidable (Final L w)] (bound : Blocklace P Wave Slot Hash → ℕ) (L : Blocklace P Wave Slot Hash) : ℕ

The finalized-wave count: the largest prefix length k (within bound L) such that every wave below k is finalized in L.

Equations

• CordialMiners.finalCountOf Final bound L = Nat.findGreatest (fun (k : ℕ) => ∀ w < k, Final L w) (bound L)

theorem CordialMiners.finalCountOf_monotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (Final : Blocklace P Wave Slot Hash → ℕ → Prop) [(L : Blocklace P Wave Slot Hash) → (w : ℕ) → Decidable (Final L w)] (bound : Blocklace P Wave Slot Hash → ℕ) (hperm : ∀ (w : ℕ) {L₁ L₂ : Blocklace P Wave Slot Hash}, L₁ ⊆ L₂ → Final L₁ w → Final L₂ w) (hbound : ∀ {L₁ L₂ : Blocklace P Wave Slot Hash}, L₁ ⊆ L₂ → bound L₁ ≤ bound L₂) {L₁ L₂ : Blocklace P Wave Slot Hash} (hsub : L₁ ⊆ L₂) : finalCountOf Final bound L₁ ≤ finalCountOf Final bound L₂

The finalized-wave count is monotone in the blocklace, given finality permanence (a finalized wave stays finalized as the blocklace grows) and a monotone bound. This is the scalar leader-safety fact of Ref.FinalizedAnchors, now derived from the canonical finality primitive.