theorem CordialMiners.threshold_certificates_agree {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') : c.value = c'.value

Byzantine agreement, the positive form of CERT-06: under honest non-equivocation and the Byzantine-weight bound, every pair of valid threshold certificates for a snapshot carries the same value. There is no fork at the certificate level.

def CordialMiners.EndToEndSafety {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] [DecidableEq Hash] (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (tau : Ordering P Wave Slot Hash) : Prop

The shared end-to-end safety conclusion: no conflicting leader ratifications, prefix-comparable outputs below a common limit, and parent closure preserved by receive-path insertion.

Equations

• One or more equations did not get rendered due to their size.

structure CordialMiners.EndToEndAssumptions {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (honest : Finset P) : Prop

The assumptions shared by the end-to-end safety variants. The ordering-specific assumption is kept separate, since each theorem discharges it from a different source.

• wf : S.WF
• byz_bound : S.ByzBound honest
• honest_non_equivocation (p : P) : p ∈ honest → ∀ (b b' : Block P Wave Slot Hash), BlockApproves L p b → BlockApproves L p b' → b = b'

theorem CordialMiners.end_to_end_safety_of_output_monotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] [DecidableEq Hash] (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (honest : Finset P) (h : EndToEndAssumptions S L honest) (tau : Ordering P Wave Slot Hash) (hmono : OutputMonotone tau) : EndToEndSafety S L tau

End-to-end safety (Theorem 4.54 core). Under the standard assumptions the protocol guarantees, in one statement: (1) leader-agreement: no two valid ratification certificates ratify conflicting target blocks; (2) output consistency: correct miners whose blocklaces sit inside a common limit produce prefix-comparable orders, so they never publish a conflicting position; (3) blocklace integrity: dissemination's receive-path preserves parent closure. The ordering's prefix-monotonicity (leader safety) enters as the hypothesis hmono, matching the blueprint's leader-safety trusted boundary.

theorem CordialMiners.topoSort_valid {H : Type u_5} [LinearOrder H] (V : Finset H) (deps : H → Finset H) {rank : H → ℕ} (hrank : ∀ (x p : H), p ∈ deps x → rank p < rank x) : (topoSort V deps).Nodup ∧ TopoSorted deps (topoSort V deps) ∧ ∀ (y : H), y ∈ topoSort V deps ↔ y ∈ V

The concrete deterministic ordering is a valid total order of its input: it is duplicate-free, topologically sorted (no dependency after its dependent), and (under the strict-rank acyclicity hypothesis) enumerates exactly the input vertices. With determinism (topoSort is a function), the deterministic-ordering requirement is met by a real, computable algorithm.

theorem CordialMiners.end_to_end_safety_of_anchor_prefix_monotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] [DecidableEq Hash] (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (honest : Finset P) (h : EndToEndAssumptions S L honest) (anchors : Blocklace P Wave Slot Hash → List Hash) (hist : Hash → List Hash) (hLead : AnchorPrefixMonotone anchors) : EndToEndSafety S L (anchoredOrder anchors hist)

End-to-end safety with the ordering hypothesis discharged. Same guarantee as end_to_end_safety_of_output_monotone, but for the concrete anchored ordering and assuming only the primitive leader-safety fact: the finalized-anchor sequence is prefix-monotone in the blocklace. Output-prefix monotonicity (TAU-08) is now derived (tau_08_anchored_output_monotone), not assumed, so the only ordering input is AnchorPrefixMonotone, which is much closer to the protocol than abstract OutputMonotone.

theorem CordialMiners.end_to_end_safety_of_finalized_count_monotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] [DecidableEq Hash] (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (honest : Finset P) (h : EndToEndAssumptions S L honest) (finalCount : Blocklace P Wave Slot Hash → ℕ) (leaderOf : ℕ → Hash) (hist : Hash → List Hash) (hCount : ∀ {L₁ L₂ : Blocklace P Wave Slot Hash}, L₁ ⊆ L₂ → finalCount L₁ ≤ finalCount L₂) : EndToEndSafety S L (anchoredOrder (finalizedAnchors finalCount leaderOf) hist)

The deepest form: end-to-end safety with a fully concrete ordering and the ordering hypothesis reduced to one scalar fact. The ordering is the anchored order over the finalized-anchor sequence, and the only ordering input is that the finalized-wave count finalCount is monotone in the blocklace (finality permanence plus wave-ordered finalization). Anchor prefix-monotonicity and output-prefix monotonicity are both derived.

theorem CordialMiners.end_to_end_safety_of_finality_permanence {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] [DecidableEq Hash] (S : CommitteeSnapshot P) (L : Blocklace P Wave Slot Hash) (honest : Finset P) (h : EndToEndAssumptions S L honest) (Final : Blocklace P Wave Slot Hash → ℕ → Prop) [(L : Blocklace P Wave Slot Hash) → (w : ℕ) → Decidable (Final L w)] (bound : Blocklace P Wave Slot Hash → ℕ) (leaderOf : ℕ → Hash) (hist : Hash → List 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₂) : EndToEndSafety S L (anchoredOrder (finalizedAnchors (finalCountOf Final bound) leaderOf) hist)

The final form: PoR-weighted Cordial Miners is safe, resting on three named facts. Given the Byzantine-weight bound (hByz), honest non-equivocation (hNoEquiv), and finality permanence (hperm: a finalized wave stays finalized as the blocklace grows), the protocol guarantees leader-agreement, output consistency, and blocklace integrity, for the fully concrete finalized-anchor ordering. The bound monotonicity (hbound) is a technical artifact satisfied by the block count. Every other ordering property (the finalized-wave count's monotonicity, anchor prefix-monotonicity, and output-prefix monotonicity) is derived.