Course-of-values recursion on the naturals, as a named kernel principle with its unfolding equation

Identifier: F:nat-strong-induction
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

If a property (or a construction, at any universe) holds at n whenever it holds at every m < n, then it holds at every n -- and the resulting function satisfies the expected unfolding equation, so a proof about it can take its first step. Both are kernel terms over Nat.lt_well_founded and the generic WellFounded.fix, with an empty axiom footprint.

Formal statement

theorem Nat.strongInduction_eq : ((x0 : ((x0 : AxNat) -> Sort (u))) -> ((x1 : ((x1 : AxNat) -> ((x2 : ((x2 : AxNat) -> ((x3 : AxNat.lt x2 x1) -> x0 x2))) -> x0 x1))) -> ((x2 : AxNat) -> Eq.{u} (x0 x2) (AxNat.strongInduction.{u} x0 x1 x2) (x1 x2 (fun (x3 : AxNat) => fun (x4 : AxNat.lt x3 x2) => AxNat.strongInduction.{u} x0 x1 x3)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 3 direct dependents

Evidence

kernel-Nat.strongInduction

Kind: kernel-term
Status: checked

Supports: the recursion principle itself, at any universe

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::subset_search_tests -- --test-threads=4

Evidence notes

The evaluation test is not decorative: a wrapper that did not reduce would type-check identically. `strongInduction (fun _ => Nat) (fun n ih => succ n) 3` must reduce to 4, which forces WellFounded.fix to reduce its accessibility proof at the numeral; 3 is named as the answer a step returning n would give.

kernel-Nat.strongInduction_eq

Kind: kernel-term
Status: checked

Supports: the unfolding equation, without which a proof about a strongly-recursive definition cannot take its first step

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::subset_search_tests -- --test-threads=4

Evidence notes

`strongInduction motive step n` does not reduce at a symbolic n -- `lt_well_founded n` is stuck -- so the equation is a genuine theorem here and not an iota rule.

shape-Nat.strongInduction

Kind: exhaustive-enumeration
Status: checked

Supports: the declaration exists under this exact name, and did not before

Checker command

cargo run --release -q -p axeyum-lean-kernel --example shape_search -- --name Nat.strongInduction --kind definition --expect 1

Evidence notes

The pre-state: at declarations=2832 with positive control Nat.Rado.IsRadoNumber FOUND, `--name-like strong` returned ABSENT, confirming ADR-1608's measurement. `Nat.base_induction` is a different statement. Nine modules in this prelude (base_induction, bezout, count_range_reversal, factorization, gcd, gcd_mul_right, irrational, totient_dvd_chain, totient_gcd_mul) already spelled the five-argument WellFounded.fix application by hand; none was rewritten by this lane.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `hall-sufficiency`: `nat_prelude/strong_induction.rs`. ADR-1614, closing ADR-1608's item 1.",
  "source": "Course-of-values induction; standard, and derivable from the well-foundedness of < which this prelude already proved (Nat.lt_well_founded, order.rs).",
  "prior_art": [
    {
      "citation": "Mathlib, `Nat.strongRecOn`",
      "establishes": "the same principle; this one is stated with an explicit motive because there is no elaborator here and every application is built positionally"
    }
  ]
}