Generalized election-timer round: fire times and uncontested rounds for arbitrary delays

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Data.Fintype.Card
import Mathlib.Logic.Equiv.Prod
import Mathlib.Order.Interval.Finset.Basic
import Mathlib.Tactic

namespace OpenSearchLivenessAbstract

/-- Fire time of candidate `i`: its offset plus its delay for draw `x i`. -/
def fireTime {n : Nat} (offset : Fin n → Int) (delay : Fin n → Fin (2 ^ 64) → Int)
    (x : Fin n → Fin (2 ^ 64)) (i : Fin n) : Int :=
  offset i + delay i (x i)

/-- A round is uncontested with margin `δ`: some candidate fires at least `δ`
before every other candidate. -/
def Uncontested {n : Nat} (offset : Fin n → Int) (delay : Fin n → Fin (2 ^ 64) → Int)
    (δ : Nat) (x : Fin n → Fin (2 ^ 64)) : Prop :=
  ∃ i, ∀ j, j ≠ i → fireTime offset delay x i + δ ≤ fireTime offset delay x j

instance {n : Nat} (offset : Fin n → Int) (delay : Fin n → Fin (2 ^ 64) → Int)
    (δ : Nat) : DecidablePred (Uncontested offset delay δ) := fun x => by
  unfold Uncontested; infer_instance

end OpenSearchLivenessAbstract