@[reducible, inline]

abbrev CordialMiners.Ordering (P : Type u_5) (Wave : Type u_6) (Slot : Type u_7) (Hash : Type u_8) : Type (max (max (max (max u_8 u_7) u_6) u_5) u_8)

An ordering function turns a blocklace into the published ordered prefix of block hashes.

Equations

• CordialMiners.Ordering P Wave Slot Hash = (CordialMiners.Blocklace P Wave Slot Hash → List Hash)

theorem CordialMiners.tau_04_deterministic {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (tau : Ordering P Wave Slot Hash) {L₁ L₂ : Blocklace P Wave Slot Hash} (h : L₁ = L₂) : tau L₁ = tau L₂

TAU-04 (determinism): an ordering is a pure function, so equal blocklaces give equal outputs. The concrete tau_ord achieves this by canonical tie-breaking at every maximum, sort, and selection.

def CordialMiners.OutputMonotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (tau : Ordering P Wave Slot Hash) : Prop

TAU-08 contract: the ordering is prefix-monotone in the blocklace. Growing the blocklace only extends the ordered output (this is what leader safety buys for the concrete algorithm).

Equations

• CordialMiners.OutputMonotone tau = ∀ {L₁ L₂ : CordialMiners.Blocklace P Wave Slot Hash}, L₁ ⊆ L₂ → tau L₁ <+: tau L₂

theorem CordialMiners.tau_10_publish_extends {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {tau : Ordering P Wave Slot Hash} (hmono : OutputMonotone tau) {L₁ L₂ : Blocklace P Wave Slot Hash} (h : L₁ ⊆ L₂) : tau L₁ <+: tau L₂

TAU-10 / IC10 (output-prefix discipline): a prefix-monotone ordering publishes only prefix extensions, so a later, larger blocklace's output extends the earlier one.

theorem CordialMiners.tau_09_output_consistent {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {tau : Ordering P Wave Slot Hash} (hmono : OutputMonotone tau) {L₁ L₂ Limit : Blocklace P Wave Slot Hash} (h₁ : L₁ ⊆ Limit) (h₂ : L₂ ⊆ Limit) : tau L₁ <+: tau L₂ ∨ tau L₂ <+: tau L₁

TAU-09 (output consistency): if two blocklaces are each a sub-blocklace of a common limit and the ordering is prefix-monotone, the two orderings are prefix-comparable. Two correct miners whose local blocklaces sit inside one limit blocklace therefore never disagree on a published position, one output is always a prefix of the other.