Mathlib v4.30 source proposition Nat.fib_two

Identifier: F:ml430-nat-fib-two-2f3715f3
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

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

Formal statement

Nat.fib 2 = 1

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-Nat.fib_two

Kind: kernel-term
Status: checked

Supports: `Nat.fib_two` is admitted as a Theorem with EXACTLY the mirror's shape, pinned verbatim via the kernel's own renderer. Proof is `Eq.refl`: `fib 2` unfolds to `fibAux 2 0 1` and reduces by delta/iota to `1`. As with `fib_one`, the RENDERED (unreduced) type is the discriminator; mutation-verified 2026-08-31 that changing the argument to `3` makes the statement FALSE and `Kernel::add_declaration` REJECTS it (the whole nat prelude build then fails).

Checker command

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

instance-Nat.fib_two

Kind: kernel-term
Status: checked

Supports: The same test, run over both names. Checks the inferred type states `Eq (fib 2) 1`, that `fib 2` reduces to `1`, and an empty axiom footprint, with the same two negative controls. Same documented limitation: it does not separate the two statements, which reduce to the same proposition.

Checker command

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

footprint-Nat.fib_two

Kind: kernel-term
Status: checked

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

Kind: kernel-term
Status: checked

Supports: Coverage for `Nat.fib_two` 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 as `Eq.refl` over the existing `Nat.fib`. 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_two` from Mathlib v4.30.0; no proof value was exposed",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.fib_two`",
      "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"
    }
  ]
}