Strong induction principles

Two well-founded recursion principles over \mathbb{N}, both derived from Nat.­strong_induction_on.

The two principles

• strong_induction_ltn — ordinary course-of-values induction on the < order.

• strong_induction_sub — induction whose well-founded measure is the gap n - k above a fixed offset k, rather than n itself.

Why a shifted measure is needed

The accountable-safety proof walks from a justified block downward along justification links toward a fixed finalized checkpoint at height k. At each step the source height strictly decreases while staying above k, so the gap (\cdot) - k strictly decreases. Ordinary induction on n cannot express this because the offset k is a fixed external parameter, not part of the recursion variable. strong_induction_sub packages exactly this pattern: it recurses on the gap n - k, with the guard k < v_{1a} ensuring the truncated subtraction is a genuine positive quantity.

Downstream use

strong_induction_sub drives the well-founded recursion of k_non_equal_height_case_ind in Theories/AccountableSafety.lean, where the induction descends on b_{1,h} - b_{2,h} as the source height strictly decreases along justification links while staying above the finalized height b_{2,h}.

Course-of-values induction on \mathbb{N}

Ordinary strong induction on \mathbb{N}:

\bigl(\forall m,\; (\forall n,\; n < m \to P\,n) \to P\,m\bigr) \;\implies\; \forall n,\; P\,n

Interpretation

The hypothesis asserts that to prove P at m, it suffices to know P holds at every strictly smaller argument. The conclusion then gives P\,n for all n. This is the standard course-of-values induction on the well-founded order < on \mathbb{N} — strictly stronger than ordinary induction because the induction hypothesis is available at all predecessors, not just m - 1.

Proof

A direct repackaging of Nat.­strong_induction_on, which provides exactly this principle from the well-foundedness of < on \mathbb{N}.

Strong induction on the gap n - k above a fixed offset

Strong induction on a shifted measure. For a fixed offset k, the predicate P holds everywhere provided each P\,v_1\,h_1 follows from P at all arguments whose gap above k is strictly smaller:

\Bigl(\forall v_1\, h_1,\;\bigl(\forall v_{1a}\, h_{1a},\; k < v_{1a} \to v_{1a} - k < v_1 - k \to P\,v_{1a}\,h_{1a}\bigr) \to P\,v_1\,h_1\Bigr) \;\implies\; \forall n\, t,\; P\,n\,t

Interpretation

The recursion measure is the gap n - k, not n itself. The guard k < v_{1a} keeps the truncated subtraction v_{1a} - k honest (strictly positive), so v_{1a} - k < v_1 - k is a genuine decrease rather than an artefact of truncation at 0.

Proof idea

Reduce to strong_induction_ltn on the quantity m = n - k: prove the auxiliary \forall m,\;\forall n\, t,\; n - k = m \to P\,n\,t by ordinary strong induction on m, then instantiate at m = n - k with rfl.

Role in the development

The induction backbone of k_non_equal_height_case_ind: walking from a justified block down its justification links, the source height drops at each step while remaining above the finalized height b_{2,h}, so the gap (\cdot) - b_{2,h} strictly decreases and the recursion is well-founded.