def CordialMiners.BlockApproves {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (L : Blocklace P Wave Slot Hash) (p : P) (target : Block P Wave Slot Hash) : Prop

A creator p ratifies a target block when it has a block in the blocklace that approves the target. Ratification weight is the weight of these ratifying creators.

Equations

• CordialMiners.BlockApproves L p target = ∃ blk ∈ L, blk.creator = p ∧ CordialMiners.ApprovesBlock L blk target

def CordialMiners.ValidRatCert {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (rc : ThresholdCert P (Block P Wave Slot Hash)) : Prop

A ratification certificate is a weighted threshold certificate whose value is the target block and whose signers are the ratifying creators. It is valid when the ratifiers are threshold-heavy and each one's block approves the target.

Equations

• CordialMiners.ValidRatCert S L rc = CordialMiners.ValidCert S (CordialMiners.BlockApproves L) rc

theorem CordialMiners.fl_block_approval_no_conflict {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {L : Blocklace P Wave Slot Hash} {a b b' : Block P Wave Slot Hash} (h : ApprovesBlock L a b) (hb' : b' ∈ L) (happ' : ApprovesBlock L a b') : ¬ConflictBlock b b'

A single block cannot approve two conflicting blocks: approving one means not observing any conflict with it, but approving the other means observing it. This is the structural reason a non-equivocating creator ratifies at most one of two conflicting targets.

theorem CordialMiners.fl_07_no_conflicting_ratifications {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] (S : CommitteeSnapshot P) (hWF : S.WF) (L : Blocklace P Wave Slot Hash) (honest : Finset P) (hNoEquiv : ∀ p ∈ honest, ∀ (b b' : Block P Wave Slot Hash), BlockApproves L p b → BlockApproves L p b' → b = b') (hByz : S.ByzBound honest) {rc rc' : ThresholdCert P (Block P Wave Slot Hash)} (hrc : ValidRatCert S L rc) (hrc' : ValidRatCert S L rc') (hconf : ConflictBlock rc.value rc'.value) : False

FL-07 (no conflicting ratifications): under the Byzantine-weight bound and honest ratification consistency, two valid ratification certificates cannot ratify conflicting target blocks. A direct corollary of CERT-06: ratification is weighted threshold approval, so the weighted-overlap safety applies unchanged.