Cassini's identity: fib(n+2)*fib(n) - fib(n+1)^2 = (-1)^(n+1), over the constructed integers

Identifier: F:cassini-identity-over-constructed-integers
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural n: fib(n+2)*fib(n) - fib(n+1)^2 = (-1)^(n+1), where fib is Nat.fib (rendered AxNat.fib in this kernel) cast into the constructed integers ℤ at each occurrence, and the subtraction, multiplication and negation are genuinely Int operations -- so this is stated over ℤ even though every fib value involved is nonnegative. THE SIGN AND THE SHIFTED EXPONENT ARE THE CONTENT: at n=0 the identity reads fib(2)*fib(0) - fib(1)^2 = 1*0 - 1 = -1 = (-1)^1, so the exponent genuinely is n+1 and not n -- a proof pinning (-1)^n instead would be a DIFFERENT, false statement for even n. Proved by induction on n via a difference-doubling step: writing D(n) := fib(n+2)*fib(n) - fib(n+1)^2, the induction step establishes D(n+1) = -D(n) using the Fibonacci recurrence fib(n+2) = fib(n) + fib(n+1) and ring identities alone (no case split, no well-founded recursion beyond the recurrence itself). This is the classical Cassini identity, restated here with no reference to matrices, determinants, or the golden ratio -- see F:cassini-as-determinant-of-a-matrix-power for the ℚ/det2 restatement that connects it to determinant multiplicativity, and that fact's notes for why phi itself is not a statable number in this kernel.

Formal statement

theorem Int.fib_cassini : ((x0 : AxNat) -> Eq.{1} Int (Int.sub (Int.mul (Int.ofNat (AxNat.fib (AxNat.succ (AxNat.succ x0)))) (Int.ofNat (AxNat.fib x0))) (Int.mul (Int.ofNat (AxNat.fib (AxNat.succ x0))) (Int.ofNat (AxNat.fib (AxNat.succ x0))))) (Int.pow (Int.neg Int.one) (AxNat.succ x0)))

Dependencies

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

16 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.fib_cassini

Kind: kernel-term
Status: checked

Supports: `Int.fib_cassini` is admitted with exactly the type quoted in `formal.statement`, read directly out of the kernel's environment via the exact `render_lean` route `int_theorem_inventory` uses. No committed test in this repository asserts `Int.fib_cassini`'s statement verbatim the way `det2_fib_is_cassini_through_det2` does for `Rat.det2_fib` or the Wilson checker does for `Int.wilson` -- this evidence row is the closest available substitute: it re-derives the rendered type from the trusted kernel on every run and fails the moment that type changes, rather than trusting the doc comment in `fibonacci.rs`.

Checker command

test "$(scripts/cargo-serialized.sh run --release -p axeyum-lean-kernel --example int_theorem_inventory -- fib_cassini 2>&1 | grep -Fc "((x0 : AxNat) -> Eq.{1} Int (Int.sub (Int.mul (Int.ofNat (AxNat.fib (AxNat.succ (AxNat.succ x0)))) (Int.ofNat (AxNat.fib x0))) (Int.mul (Int.ofNat (AxNat.fib (AxNat.succ x0))) (Int.ofNat (AxNat.fib (AxNat.succ x0))))) (Int.pow (Int.neg Int.one) (AxNat.succ x0)))")" -ge 1

Evidence notes

Run 2026-08-24 against this tree: exit 0. A deliberately wrong substring (a string that appears nowhere in the tool's output) run through the identical command exits 1, confirming the grep is not a vacuous pass. This is the strongest available check that does not require adding a new pinned test to `crates/`, which this lane's brief forbids touching.

footprint-Int.fib_cassini

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for Int.fib_cassini. `derived_laws_have_no_axiom_footprint` iterates the fixed-size `derived_laws` array (122 entries, a compile-time-checked size so an omission cannot silently pass) which includes `p.fib_cassini`, and requires `Kernel::axiom_footprint` to be empty for every entry. The `integer` prelude's trusted surface is 0: no Axiom, no Opaque, no Quotient.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib int_prelude::int_prelude_tests::derived_laws_have_no_axiom_footprint -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Run 2026-08-24: `test result: ok. 1 passed; 0 failed`, exit 0. Running the identical command against a deliberately misspelled test path (`..._axiom_footprint_WRONG_NAME`) exits 1 with `error: no test with the name...` / zero matched, confirming the anchor cannot read a no-op as success.

Provenance

{
  "date": "2026-08-24",
  "established_by": "lane agent-correspondence-cassini (2026-08-24), closing ADR-0546's motivating example. Int.fib_cassini itself was proved by an earlier lane (see fibonacci.rs); this lane's contribution is making the already-admitted theorem an addressable fact in the ledger, with its statement read from the kernel rather than transcribed from a doc comment.",
  "sources": [
    "crates/axeyum-lean-kernel/src/int_prelude/fibonacci.rs",
    "crates/axeyum-lean-kernel/src/int_prelude.rs",
    "crates/axeyum-lean-kernel/src/int_prelude/int_prelude_tests.rs"
  ],
  "prior_art": [
    {
      "who": "Giovanni Domenico Cassini",
      "what": "the identity relating three consecutive Fibonacci numbers",
      "year": 1680,
      "where": "conventionally attributed",
      "attribution": "standard attribution; this lane did not consult a primary source."
    }
  ]
}