Justification and finalization: structural lemmas

Lemmas connecting the definitional layer (AtomicDef/Justification.lean) to the safety and liveness theories. Two groups:

Monotonicity under state extension

• supermajority_weaken — a supermajority link in \sigma survives in any extension \sigma' \supseteq \sigma (provided the extension satisfies the vote well-formedness property).

• justified_weaken — justification is likewise monotone under state extension: every justified block in \sigma remains justified in \sigma'. Proved by induction on the justified derivation, applying supermajority_weaken at each link.

These two lemmas are the mechanism by which the plausible-liveness construction (plausible_liveness_construct_extension) carries justification from the old state into the extended state.

The finalized ↔ k-finalized bridge

• k_finalized_means_justified — every k-finalized block is justified (extract the n = 0 component of the chain).

• finalized_means_justified_child — a finalized block has a justified child at height h + 1.

• finalized_means_one_finalized — the equivalence \operatorname{finalized} \iff \operatorname{k\_finalized}\,1.

• k_finalized_last_justified — the last block in a k-finalization chain is justified and reachable by exactly k parent steps.

• justified_cases — case analysis on a justified derivation: either genesis or a link from a justified source.

Supermajority links survive state extension

Supermajority links are monotone under state extension:

\sigma \subseteq \sigma' \;\wedge\; \operatorname{wf}(\sigma') \;\wedge\; \operatorname{supermajority\_link}(\sigma, s, t, h_s, h_t) \;\implies\; \operatorname{supermajority\_link}(\sigma', s, t, h_s, h_t)

where \sigma \subseteq \sigma' means every vote in \sigma is in \sigma', and \operatorname{wf}(\sigma') abbreviates votes_from_target_vset_property.

Proof idea

The supporter set \operatorname{link\_supporters}(\sigma, s, t, h_s, h_t) is a subset of \operatorname{link\_supporters}(\sigma', s, t, h_s, h_t) (since every old vote persists in \sigma'). The larger supporter set still lies in V(t) by the well-formedness hypothesis on \sigma'. quorum_2_upclosed then transfers the quorum property from the smaller to the larger set.

Assumptions

• \sigma \subseteq \sigma' — vote-level inclusion HSub;

• \operatorname{wf}(\sigma') — well-formedness of the target state hwf;

• \operatorname{supermajority\_link}(\sigma, s, t, h_s, h_t) — the link is already a supermajority link in \sigma hsm.

Non-assumptions

• the well-formedness of \sigma is not needed — only that of \sigma', since it is the grown supporter set whose eligibility must be checked;

• nothing about the height pair (h_s, h_t) or the block-tree relation between s and t is used: this lemma concerns only the weight/eligibility of the supporters, treating the link's graph data as opaque.

Role in the development

The mechanism by which justified_weaken carries each justification link across the state extension, and by which supermajority_link_of_quorum_votes constructs new links in the extended state. It is the single point where the quorum up-closure quorum_2_upclosed meets the protocol's monotone vote accumulation.

Justified blocks remain justified in any extension

Justification is monotone under state extension:

\sigma \subseteq \sigma' \;\wedge\; \operatorname{wf}(\sigma') \;\wedge\; \operatorname{justified}(\sigma, t, h_t) \;\implies\; \operatorname{justified}(\sigma', t, h_t)

Every block justified in \sigma remains justified in any well-formed extension \sigma'.

Proof idea

Induction on the justified derivation (.rec). The genesis case is immediate (genesis is justified in every state). In the link case, the induction hypothesis gives \operatorname{justified}(\sigma', s, h_s) for the source; the three conjuncts of the justification link are carried across as follows: the height guard h_s < h_t and the ancestry s \xrightarrow{h_t - h_s} t are state-independent (they depend only on the block tree), and the supermajority link is transferred by supermajority_weaken.

Assumptions

• \sigma \subseteq \sigma' — every vote of the old state persists HSub (this is a vote-level inclusion, not a supporter-set or weight inclusion — those are derived);

• \operatorname{wf}(\sigma') — well-formedness of the target state hwf (votes_from_target_vset_property), needed by supermajority_weaken to keep the enlarged supporter set inside V(t);

• \operatorname{justified}(\sigma, t, h_t) — the block is justified in the old state hj.

Non-assumptions

• well-formedness of the old state \sigma is not required — only \sigma' must be well-formed, because the supporter set grows and it is the larger set that must stay within V(t);

• the new votes \sigma' \setminus \sigma are entirely unconstrained beyond well-formedness — they may support arbitrary other links;

• monotonicity is one-directional: it says nothing about justification being preserved under shrinking (which is false in general).

Role in the development

Used in plausible_liveness_construct_extension to carry the highest justified block's justification from \sigma into the extended state \sigma' — the guarantee that adding the two new quorums' votes never un-justifies the existing frontier.

The finalized ↔ k-finalized bridge

The next five lemmas connect finalized (one-step, defined in AtomicDef/Justification.lean) with k_finalized (depth-k). Their roles are:

Justification extraction

k_finalized_means_justified — the base block of any k-finalization chain is justified.

Child extraction

finalized_means_justified_child — a finalized block has a justified child at height h + 1.

The equivalence

finalized_means_one_finalized — finalized \iff 1-finalized.

Last-block extraction

k_finalized_last_justified — the chain's last block is justified and reachable in exactly k steps.

Case analysis

justified_cases — inversion on the justified inductive, surfacing genesis vs link as a disjunction.

The base block of a k-finalization chain is justified

k-finalization implies justification: the base block of a k-finalization chain is justified.

\operatorname{k\_finalized}(\sigma, b, b_h, k) \;\implies\; \operatorname{justified}(\sigma, b, b_h)

Proof idea

The definition of k_finalized includes a universal quantifier \forall n \le k, asserting that each chain block \operatorname{ls.getD}\,n\,b is justified at height b_h + n. Instantiating at n = 0 (which satisfies 0 \le k by Nat.zero_le) gives \operatorname{justified}(\sigma, \operatorname{ls.getD}\,0\,b, b_h + 0). The list accessor at index 0 agrees with the head (\operatorname{ls.getD}\,0\,b = \operatorname{ls.headD}\,b = b$ by {lit}listgetDzeroeqheadD and the chain's head condition), and $bh + 0 = bh$ by Nat.add_zero, so two Eq.subst transports yield the result.

Role in the development

Used wherever a k-finalized block's justification is needed: k_equal_height_case, k_non_equal_height_case, and no_k_finalized_justified_same_height in the safety development.

A finalized block has a justified child at the next height

A finalized block has a justified child:

\operatorname{finalized}(\sigma, p, p_h) \;\implies\; \exists\, c,\; p \to c \;\wedge\; \operatorname{justified}(\sigma, c, p_h + 1)

Proof idea

From the finalization data (p, c, p_h) — where p is justified at p_h, p \to c, and there is a supermajority link from (p, p_h) to (c, p_h + 1) — the child's justification is constructed by applying the justified_link rule. This requires assembling the justification-link triple:

• forward direction p_h < p_h + 1 (by Nat.lt_succ_self),

• graded ancestry p \xrightarrow{1} c (by parent_ancestor applied to p \to c, with the distance rewritten from (p_h + 1) - p_h = 1 via add_one_sub_self),

• the supermajority link (given directly).

Role in the development

Not directly consumed by the safety or liveness theorems, but provides a useful derived fact: finalization at p_h gives a justified block one level higher, bridging finalization to the next height layer.

One-step finalization is equivalent to 1-finalization

Finalized \iff 1-finalized: the one-step finalization definition finalized is equivalent to \operatorname{k\_finalized} with k = 1:

\operatorname{finalized}(\sigma, b, b_h) \;\iff\; \operatorname{k\_finalized}(\sigma, b, b_h, 1)

Forward direction

Given finalized data (b, c, b_h) with b \to c and supermajority link from (b, b_h) to (c, b_h + 1), constructs the chain [b, c] of length 2 = 1 + 1. The quantifier \forall n \le 1 is split into n = 0 and n = 1 by leq_one_means_zero_or_one; the n = 0 case gives b's justification, the n = 1 case gives c's justification and the parent-as-graded-ancestry fact via parent_ancestor.

Reverse direction

Extracts b's justification from the n = 0 component, recovers the parent edge from the n = 1 ancestry via parent_ancestor, and reads the supermajority link from the chain's last-block component (converting via list_getLastD_eq_getD_one_of_length_two).

The last block of a k-finalization chain is justified and reachable

Last block of a k-finalization chain: the chain's endpoint is justified, reachable by exactly k parent steps, and carries the closing supermajority link.

\operatorname{k\_finalized}(\sigma, b, b_h, k) \;\implies\; \exists\, \mathit{last},\; \operatorname{justified}(\sigma, \mathit{last}, b_h + k) \;\wedge\; b \xrightarrow{k} \mathit{last} \;\wedge\; \operatorname{supermajority\_link}(\sigma, b, \mathit{last}, b_h, b_h + k)

The witness is \operatorname{ls.getLastD}\,b, converted to the positional accessor \operatorname{ls.getD}\,k\,b via list_getLastD_eq_getD_of_length_eq_succ, so that the chain's universal quantifier at n = k supplies the justification and ancestry components.

Used in k_slash_surround_case_general to extract the last justified block of the finalization chain for comparison with a conflicting justification link target.

A justified block is either genesis or reached by a link

Case analysis on justification: a justified block is either genesis at height 0, or it was reached via a justification link from a justified source:

\operatorname{justified}(\sigma, b, b_h) \;\implies\; (b = g \;\wedge\; b_h = 0) \;\lor\; \exists\, s\, s_h,\; \operatorname{justified}(\sigma, s, s_h) \;\wedge\; \operatorname{justification\_link}(\sigma, s, b, s_h, b_h)

Interpretation

This is a direct match on the two constructors of justified (justified_genesis and justified_link), surfacing the inductive structure as a proposition-level disjunction. The genesis case identifies the block as g at height 0; the link case provides the predecessor s at height s_h, its justification proof, and the full justification link from s to b.

Role in the development

The standard entry point for case-splitting on justification in every branch of the safety argument:

• two_justified_same_height_slashed — the same-height slashing kernel uses it on both blocks;

• k_non_equal_height_case_ind — the strong-induction step uses it to extract the predecessor link;

• maximal_link_highest_block — uses it to show that a justified block above the maximal-link target would produce a higher link, contradicting maximality.