def CordialMiners.anchoredOrder {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (anchors : Blocklace P Wave Slot Hash → List Hash) (hist : Hash → List Hash) : Ordering P Wave Slot Hash

The anchored ordering: concatenate, in finalized-leader order, each anchor's committed causal history. anchors L is the sequence of finalized leader hashes; hist a is the canonical ordered committed history below anchor a, which is fixed once a is finalized.

Equations

• CordialMiners.anchoredOrder anchors hist L = List.flatMap hist (anchors L)

def CordialMiners.AnchorPrefixMonotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (anchors : Blocklace P Wave Slot Hash → List Hash) : Prop

Leader safety, isolated: as the blocklace grows, the finalized-anchor sequence extends as a prefix. Finalized leaders are permanent and ordered by wave, so newly finalized leaders append after the existing ones rather than reordering them.

Equations

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

theorem CordialMiners.tau_08_anchored_output_monotone {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (anchors : Blocklace P Wave Slot Hash → List Hash) (hist : Hash → List Hash) (hmono : AnchorPrefixMonotone anchors) : OutputMonotone (anchoredOrder anchors hist)

TAU-08 discharged: when the anchor sequence is prefix-monotone (leader safety), the anchored ordering is output-monotone. Each anchor's committed history is fixed, so extending the anchor sequence only appends more blocks to the output, never reorders the published prefix.