Mathlib v4.30 source proposition Int.fib_two_mul_add_two

Identifier: F:ml430-int-fib-two-mul-add-two-0ba4a948
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The proposition declared as `Int.fib_two_mul_add_two` in the pinned Mathlib v4.30 source.

Formal statement

∀ (n : ℤ), Int.fib (2 * n + 2) = Int.fib (n + 1) * (2 * Int.fib n + Int.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-Int.fib_two_mul_add_two

Kind: kernel-term
Status: checked

Supports: Int.fib_two_mul_add_two is admitted by the trusted kernel gate, and its canonical type is the pinned Mathlib statement symbol for symbol: ((x0 : Int) -> Eq.{1} Int (Int.fib (Int.add (Int.mul (Int.ofNat (AxNat.succ (AxNat.succ AxNat.zero))) x0) (Int.ofNat (AxNat.succ (AxNat.succ AxNat.zero))))) (Int.mul (Int.fib (Int.add x0 Int.one)) (Int.add (Int.mul (Int.ofNat (AxNat.succ (AxNat.succ AxNat.zero))) (Int.fib x0)) (Int.fib (Int.add x0 Int.one))))).

Checker command

cargo run -q --release -p axeyum-lean-kernel --example int_theorem_inventory -- fib_two_mul_add_two 2>/dev/null | grep -cE '^theorem[[:space:]]+Int\.fib_two_mul_add_two[[:space:]]+\(\(x0[[:space:]]+:[[:space:]]+Int\)[[:space:]]+->[[:space:]]+Eq\.\{1\}[[:space:]]+Int[[:space:]]+\(Int\.fib[[:space:]]+\(Int\.add[[:space:]]+\(Int\.mul[[:space:]]+\(Int\.ofNat[[:space:]]+\(AxNat\.succ[[:space:]]+\(AxNat\.succ[[:space:]]+AxNat\.zero\)\)\)[[:space:]]+x0\)[[:space:]]+\(Int\.ofNat[[:space:]]+\(AxNat\.succ[[:space:]]+\(AxNat\.succ[[:space:]]+AxNat\.zero\)\)\)\)\)[[:space:]]+\(Int\.mul[[:space:]]+\(Int\.fib[[:space:]]+\(Int\.add[[:space:]]+x0[[:space:]]+Int\.one\)\)[[:space:]]+\(Int\.add[[:space:]]+\(Int\.mul[[:space:]]+\(Int\.ofNat[[:space:]]+\(AxNat\.succ[[:space:]]+\(AxNat\.succ[[:space:]]+AxNat\.zero\)\)\)[[:space:]]+\(Int\.fib[[:space:]]+x0\)\)[[:space:]]+\(Int\.fib[[:space:]]+\(Int\.add[[:space:]]+x0[[:space:]]+Int\.one\)\)\)\)\)$'

Evidence notes

The pattern pins the ENTIRE rendered type, not just the name, so swapping which `fib` factor is doubled (`fib(n+1)*(2*fib n + fib(n+1))` vs `fib n*(2*fib(n+1) + fib n)`) cannot pass. Verified discriminating on this tree: 1 against the real row, 0 against a row with the two `Int.fib (Int.add x0 Int.one)` / `Int.fib x0` occurrences swapped in the second factor. Tab separators matched with `[[:space:]]`, never `\t`. `--release` is MANDATORY: this binary also builds creal/complex/cpoint, which overflow the default debug thread stack, and a debug run's empty output would read as ABSENT.

footprint-Int.fib_two_mul_add_two

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.fib_two_mul_add_two

Checker command

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

Evidence notes

Re-measured on this tree: integer trusted surface = 0. --require-axiom-free exits nonzero when the count is not zero, so the exit status depends on the finding. --release is MANDATORY: this binary also builds creal/complex/cpoint, which overflow the default debug thread stack, and a debug run's empty output would read as ABSENT.

evaluation-Int.fib_two_mul_add_two-each-sign

Kind: witness-replay
Status: checked

Supports: fib_two_mul_add_two instantiated at n=5 (fib(12)=144=fib(6)*(2*fib(5)+fib(6))=8*18) and n=-3 (fib(-4)=-3=fib(-2)*(2*fib(-3)+fib(-2))=(-1)*3), each paired with the value the factors-swapped formula fib(n)*(2*fib(n+1)+fib(n)) gives (105 and 0 respectively), which must NOT be def_eq.

Checker command

test "$(cargo test -q -p axeyum-lean-kernel --lib int_prelude::int_prelude_tests::fib_two_mul_add_two_computes_at_a_concrete_index_of_each_sign 2>/dev/null | grep -cE '^test result: ok\. 1 passed')" -eq 1

Evidence notes

crates/axeyum-lean-kernel/src/int_prelude/int_prelude_tests.rs. The command asserts EXACTLY ONE test passed, so a filter matching nothing fails rather than exiting 0.

Provenance

{
  "date": "2026-08-29",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/fibonacci.rs, declare_fib_two_mul_add_two)",
  "prior_art": [
    {
      "attribution": "the proposition statement was read from the pinned statement-only inventory; the proof PRODUCED here is this kernel's own construction (Int.fib_add at (n+1,n+1) plus Int.fib_rec and ring algebra), not a transcription of Mathlib's tactic proof, which was never consulted.",
      "what": "the theorem declaration `Int.fib_two_mul_add_two`",
      "where": "mathlib4 commit c5ea00351c28e24afc9f0f84379aa41082b1188f (v4.30.0)",
      "who": "the Mathlib contributors",
      "year": 2026
    }
  ],
  "source": "proved in-tree over the CONSTRUCTED integers. The canonical type was read from int_theorem_inventory's own output and compared symbol for symbol against the pinned Mathlib statement already recorded in formal.statement, which is unchanged."
}