structure CordialMiners.ThresholdCert (P : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

A weighted threshold certificate for a candidate value: the value and the set of signers. The cryptographic evidence (one approval signature per signer) is abstracted into the approved predicate of ValidCert; the weight argument is what the safety proof turns on.

• value : V
• signers : Finset P

def CordialMiners.ValidCert {P : Type u_1} {V : Type u_2} (S : CommitteeSnapshot P) (approved : P → V → Prop) (c : ThresholdCert P V) : Prop

A certificate is valid for a snapshot and an approval relation when its signer set is threshold-heavy and every signer approved the certificate's value.

Equations

• CordialMiners.ValidCert S approved c = (S.Heavy c.signers ∧ ∀ p ∈ c.signers, approved p c.value)

theorem CordialMiners.cert_05_heavy_overlap {P : Type u_1} [DecidableEq P] (S : CommitteeSnapshot P) (hWF : S.WF) {A B : Finset P} (hA : S.Heavy A) (hB : S.Heavy B) : 2 * (S.threshold.num * S.totalWeight) < wt S.weight (A ∩ B) * S.threshold.den + S.totalWeight * S.threshold.den

CERT-05: two threshold-heavy signer sets overlap beyond (2θ − 1)W of the committee weight. The snapshot-level restatement of FOUND-05, the basis of no-conflicting-finals.