Mathlib v4.30 source proposition Nat.fib_add

Identifier: F:ml430-nat-fib-add-81ea2485
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

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

Formal statement

∀ (m n : ℕ), Nat.fib (m + n + 1) = Nat.fib m * Nat.fib n + Nat.fib (m + 1) * Nat.fib (n + 1)

Dependencies

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

9 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Nat.fib_add

Kind: kernel-term
Status: checked

Supports: `Nat.fib_add` is admitted as a Theorem with EXACTLY the mirror's shape, pinned verbatim via the kernel's own renderer (`fib (succ (m + n))` is Mathlib's `fib (m + n + 1)`; `fib (succ m)` is `fib (m + 1)`). Declared in `fibonacci.rs` by an induction that proves the statement at `n` and `succ n` together, the successor step folding two `fib_add_two` applications.

Checker command

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

instance-Nat.fib_add

Kind: kernel-term
Status: checked

Supports: Checks the statement at genuinely FREE `m` and `n` in an explicit `LocalContext` -- the discriminating check, since at concrete numerals both sides collapse to one literal -- with a symbolic negative control replacing the second product's first factor by `fib m`. Also evaluates concretely at `(3, 4)`: `fib 8 = 21 = 2*3 + 3*5`. Records what the concrete point does NOT rule out: at `(3,4)` the transposed product order also evaluates to 21, so only the symbolic check separates the orderings.

Checker command

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

footprint-Nat.fib_add

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for `Nat.fib_add`. 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_add

Kind: kernel-term
Status: checked

Supports: Coverage for `Nat.fib_add` 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): the declaration already existed in nat_prelude/fibonacci.rs; this lane compared its RENDERED kernel type against the mirror's formal.statement, added the missing instantiation test, and flipped the status. No proof work. 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_add` from Mathlib v4.30.0; no proof value was exposed",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.fib_add`",
      "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"
    }
  ]
}