Structural lemmas for ancestry

This file collects the closure properties of the two ancestry relations defined in AtomicDef/HashTree.lean: the ungraded hash_ancestor (\xrightarrow{*}) and the distance-indexed nth_ancestor (\xrightarrow{n}).

Closure properties of \xrightarrow{*}

The relation hash_ancestor satisfies:

• Reflexivity — hash_self_ancestor: h \xrightarrow{*} h

• Transitivity — hash_ancestor_concat: h_1 \xrightarrow{*} h_2 \xrightarrow{*} h_3 \implies h_1 \xrightarrow{*} h_3

• One-step extension on either end — hash_ancestor_stepL (prepend a parent edge) and hash_ancestor_stepR (append; the step constructor itself)

• Proper embedding of a parent edge — hash_parent_ancestor: a single parent edge h_1 \to h_2 gives both ancestry and distinctness h_1 \ne h_2 (from irreflexivity of hash_parent_irreflexive)

Conflict propagation

hash_ancestor_conflict is the contrapositive of transitivity: if h_1 \xrightarrow{*} h_2 and p is not an ancestor of h_2, then p is not an ancestor of h_1 either. Together with hash_nonancestor_nonequal (non-ancestry implies distinctness), this lets the safety proofs rule out branch configurations by propagating non-ancestry upward along justification chains.

Graded–ungraded interface

• nth_ancestor_ancestor — forgets the distance index: \xrightarrow{n} implies \xrightarrow{*}

• nth_ancestor_0_refl — distance 0 forces equality

• parent_ancestor — a parent edge is exactly distance-1 ancestry (\leftrightarrow)

• nth_ancestor_succ_inv — successor inversion: a distance-(n+1) chain decomposes as a distance-n chain followed by one parent edge, extracting the penultimate block

Downstream use

The conflict lemmas feed the safety case analysis in Theories/AccountableSafety.lean (k_safety', k_non_equal_height_case_ind); parent_ancestor and nth_ancestor_succ_inv feed the finalization bridge finalized_means_one_finalized and the block-existence extraction blocks_exist_extract_new_final_pair_from_bound.

Every block is its own ancestor

Reflexivity of the ancestry relation \xrightarrow{*}:

\forall\, h,\; h \xrightarrow{*} h

Every block is its own ancestor — the zero-length path. This is the refl constructor of hash_ancestor, exposed as a lemma. It is the base case for any ancestry argument: in particular, it supplies the starting path in hash_ancestor_stepL and hash_parent_ancestor.

A parent edge is a proper ancestry step

A parent edge gives ancestry and distinctness: from h_1 \to h_2 together with the irreflexivity hypothesis on the parent relation,

h_1 \xrightarrow{*} h_2 \;\wedge\; h_1 \ne h_2

The ancestry half comes from one step over refl; the distinctness half is exactly hash_parent_irreflexive applied to the edge.

Ancestry paths compose by transitivity

Transitivity of \xrightarrow{*}:

h_1 \xrightarrow{*} h_2 \;\wedge\; h_2 \xrightarrow{*} h_3 \;\implies\; h_1 \xrightarrow{*} h_3

Proved by induction on the second path h_2 \xrightarrow{*} h_3, extending h_1 \xrightarrow{*} h_2 one edge at a time via the step constructor. The base case (refl) returns the first path unchanged.

Prepending a parent edge extends ancestry

Prepend a parent edge on the left: h_1 \to h_2 and h_2 \xrightarrow{*} h_3 give h_1 \xrightarrow{*} h_3. Obtained by concatenating the single-step path h_1 \xrightarrow{*} h_2 (from step over refl) with the given path via hash_ancestor_concat.

Appending a parent edge extends ancestry

Append a parent edge on the right: h_1 \xrightarrow{*} h_2 and h_2 \to h_3 give h_1 \xrightarrow{*} h_3. This is the step constructor of hash_ancestor exposed as a lemma.

Non-ancestors are distinct blocks

Non-ancestry implies distinctness:

\neg\,(h_1 \xrightarrow{*} h_2) \;\implies\; h_1 \ne h_2

The contrapositive of reflexivity: if h_1 = h_2 held, then h_1 \xrightarrow{*} h_1 (by hash_self_ancestor) would be transported via Eq.subst to h_1 \xrightarrow{*} h_2, contradicting the non-ancestry hypothesis. Used in k_safety' to derive b_1 \ne b_2 from mutual non-ancestry of two k-finalized blocks.

Non-ancestry propagates upward along paths

Conflict propagation — the contrapositive of transitivity:

h_1 \xrightarrow{*} h_2 \;\wedge\; \neg\,(p \xrightarrow{*} h_2) \;\implies\; \neg\,(p \xrightarrow{*} h_1)

If p cannot reach h_2, and h_1 can, then p cannot reach h_1 either — because if it could, composing the two paths via hash_ancestor_concat would give p \xrightarrow{*} h_2, contradicting the second hypothesis.

This is the key lemma that propagates non-ancestry upward along justification chains in k_non_equal_height_case_ind: as the induction descends from a justified block toward the finalized checkpoint, the non-ancestry hypothesis is carried to each predecessor source.

Graded–ungraded interface

The following lemmas connect the distance-indexed nth_ancestor (\xrightarrow{n}) with the ungraded hash_ancestor (\xrightarrow{*}). The key facts are:

Forgetting the index

nth_ancestor_ancestor: \xrightarrow{n} implies \xrightarrow{*}

Base cases

nth_ancestor_0_refl (n = 0 \implies equality) and parent_ancestor (n = 1 \iff parent edge)

Inversion

nth_ancestor_succ_inv: a distance-(n+1) chain splits as a distance-n chain plus one parent edge

Distance-indexed ancestry implies ungraded ancestry

A distance-n chain gives an ungraded ancestry path, forgetting the step count:

s \xrightarrow{n} t \;\implies\; s \xrightarrow{*} t

Proved by induction on the nth_ancestor derivation: the base case (nth_ancestor_0) gives refl, the step case (nth_ancestor_nth) extends by step.

Zero-step ancestry forces equality

h_1 \xrightarrow{0} h_2 implies h_1 = h_2. The only constructor producing distance 0 is nth_ancestor_0, which requires h_1 = h_2.

A parent edge is exactly one-step graded ancestry

A parent edge is exactly a graded ancestry step of length one:

h_1 \to h_2 \;\iff\; h_1 \xrightarrow{1} h_2

The forward direction builds nth_ancestor_nth over nth_ancestor_0; the reverse matches on the single-step chain and extracts the parent edge. Used in finalized_means_one_finalized and finalized_means_justified_child to convert between the parent edge in finalized and the graded ancestry in k_finalized.

A distance-(n+1) chain splits into a chain plus one edge

Successor inversion: a distance-(n+1) chain decomposes as a distance-n chain followed by one parent edge:

a \xrightarrow{n+1} c \;\implies\; \exists\, b,\; a \xrightarrow{n} b \;\wedge\; b \to c

The proof matches on the nth_ancestor_nth constructor, which is the only one producing \mathrm{succ}\,n, and extracts the intermediate block b together with the two halves of the chain. Used in blocks_exist_extract_new_final_pair_from_bound to peel the last parent edge off a block-existence witness.