theorem CordialMiners.cert_06_no_conflicting_threshold_finals {P : Type u_1} {V : Type u_2} [DecidableEq P] (S : CommitteeSnapshot P) (hWF : S.WF) (approved : P → V → Prop) (honest : Finset P) (hNoEquiv : ∀ p ∈ honest, ∀ (v v' : V), approved p v → approved p v' → v = v') (hByz : S.ByzBound honest) {c c' : ThresholdCert P V} (hc : ValidCert S approved c) (hc' : ValidCert S approved c') (hconf : c.value ≠ c'.value) : False

CERT-06 (no conflicting threshold finals). Under honest non-equivocation and the Byzantine-weight bound S.ByzBound honest, two valid threshold certificates for the same snapshot cannot carry conflicting (distinct) values. Threshold finality is therefore self-enforcing: it needs no health assumption, only the adversary bound and that honest members do not sign two values.