Mathlib v4.30 source proposition Nat.fib_lt_fib_succ

Identifier: F:ml430-nat-fib-lt-fib-succ-b4305b68
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The proposition declared as `Nat.fib_lt_fib_succ` in the pinned Mathlib v4.30 source.

Formal statement

∀ {n : ℕ}, 2 ≤ n → Nat.fib n < Nat.fib (n + 1)

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

kernel-Nat.fib_lt_fib_succ

Kind: kernel-term
Status: checked

Supports: `Nat.fib_lt_fib_succ` is admitted as a Theorem with EXACTLY the mirror's shape, pinned verbatim via the kernel's own renderer. One `Iff.mpr` against the already-proved `Nat.fib_lt_fib` (`2 <= m -> (fib m < fib n <-> m < n)`) instantiated at `(n, succ n)`, with `Nat.lt_succ_self` supplying the reverse direction's premise. No induction.

Checker command

test "$(cargo run -q --release -p axeyum-lean-kernel --example nat_theorem_inventory fib_lt_fib_succ 2>/dev/null | awk -F'\t' '$1 == "Nat.fib_lt_fib_succ" && $3 == "((x0 : AxNat) -> ((x1 : AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x0) -> AxNat.lt (AxNat.fib x0) (AxNat.fib (AxNat.succ x0))))"' | wc -l)" -ge 1

instance-Nat.fib_lt_fib_succ

Kind: kernel-term
Status: checked

Supports: Applies at a concrete `n = 2` (hypothesis `Le 2 2` by `le_refl`, conclusion `Lt (fib 2) (fib 3)`) AND at a genuinely free `n` pushed into an explicit `LocalContext`. Negative control: the TRANSPOSED conclusion `Lt (fib (succ n)) (fib n)` is rejected, and it is not vacuous -- at `n = 2` it reads `2 < 1`, which is false. The `2 <= n` hypothesis is shown load-bearing NUMERICALLY: `fib 1` and `fib 2` are both `1`, so the unconditional form would claim `1 < 1`.

Checker command

test "$(cargo test -p axeyum-lean-kernel --lib nat_prelude::fib_extra_tests::fib_lt_fib_succ_applies_concretely_and_symbolically_and_needs_its_hypothesis -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

footprint-Nat.fib_lt_fib_succ

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for `Nat.fib_lt_fib_succ`. The `nat` prelude's trusted surface stays 0: no Axiom, no Opaque, no Quotient.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free nat

coverage-Nat.fib_lt_fib_succ

Kind: kernel-term
Status: checked

Supports: Coverage for `Nat.fib_lt_fib_succ` derived from `kernel.environment()` directly, not from an inventory list -- a Nat-namespace declaration missing from `theorem_names` fails this test by name.

Checker command

test "$(cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::every_nat_declaration_is_checked_and_axiom_free -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Provenance

{
  "date": "2026-08-29",
  "established_by": "lane mirror-frontier-2 (2026-08-31): declared in the new file nat_prelude/fib_extra.rs from the already-proved `Nat.fib_lt_fib` at `(n, succ n)` plus `Nat.lt_succ_self`. Verified against the pinned Mathlib v4.30.0 source (commit c5ea00351c28e24afc9f0f84379aa41082b1188f) that `Nat.fib` there is `((fun p => (p.snd, p.fst + p.snd))^[n] (0, 1)).fst` (Mathlib/Data/Nat/Fib/Basic.lean:57) -- the SAME accumulator-pair iteration from the SAME seed (0,1) that this kernel's `fib n := fibAux n 0 1` runs, curried across two argument slots because this kernel has no tuple type. Same function, same algorithm, different representation of the pair, so the mirror is our statement and flipping it is honest under the mirror-flip criterion. Mathlib proves its own fib_zero/fib_one/fib_two by `rfl` (Basic.lean:61-69), so those are definitional on its side exactly as here -- the Stirling precedent. This corrects ADR-0840's point 4, which described Mathlib's `fib` as a two-step Nat.rec/well-founded recurrence; that half of the ADR cited only this repository's own module doc, not the pinned source. The mirror-divergence registry agrees: `Nat.fastFib` is a registered divergence, `Nat.fib` is not.",
  "source": "statement-only extraction of `Nat.fib_lt_fib_succ` from Mathlib v4.30.0; no proof value was exposed",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.fib_lt_fib_succ`",
      "where": "mathlib4 commit c5ea00351c28e24afc9f0f84379aa41082b1188f (v4.30.0)",
      "year": 2026,
      "attribution": "the proposition was read from the pinned statement-only inventory; the proof term and tactic trace were not consulted"
    }
  ]
}