Cassini's identity restated through det2: det2 applied to the ofInt-cast Fibonacci entries equals ofInt((-1)^(n+1))

Identifier: F:cassini-as-determinant-of-a-matrix-power
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural n: det2 (ofInt (fib(n+2))) (ofInt (fib(n+1))) (ofInt (fib(n+1))) (ofInt (fib n)) = ofInt ((-1)^(n+1)), over the constructed rationals ℚ, where ofInt : ℤ -> ℚ is Rat.ofInt (the ring embedding) and fib is Nat.fib cast into ℤ. Read through det2's definition (det2 x y z w := x*w - y*z), the left side is exactly Cassini's identity's left side, fib(n+2)*fib(n) - fib(n+1)^2, cast termwise into ℚ -- and the four entries are exactly the entries of M^n for M = [[1,1],[1,0]] (M^n = [[fib(n+1), fib n],[fib n, fib(n-1)]] for n >= 1, extended to n=0 by M^0 = I), so this restates Cassini's identity as det(M^n) = (-1)^n for the specific matrix whose powers generate consecutive Fibonacci numbers. THIS FACT IS DERIVED FROM F:cassini-identity-over-constructed-integers, NOT reproved independently: the kernel proof transports Int.fib_cassini across Rat.ofInt using three ring-homomorphism lemmas (Rat.ofInt_add, Rat.ofInt_mul, Rat.ofInt_neg) and rewrites the cast difference into det2's applied form. IT DOES NOT USE Rat.det2_mul AT ALL -- confirmed by reading the proof term's direct dependencies, which are exactly Int.fib_cassini, Rat.ofInt_add, Rat.ofInt_mul, Rat.ofInt_neg. So while the CLASSICAL argument for why Cassini and determinant multiplicativity are one theorem goes through M, M^n and det2_mul applied n times with det2_id as the base case, THIS KERNEL'S PROOF of the present fact is a direct algebraic transport of Cassini and cites det2_mul nowhere: no matrix, matrix power, or matrix product is ever reified as a value (this kernel has no product/tuple type), and the identification of the four entries with M^n's entries is read off by a human, not mechanized as an induction over matrix powers.

Formal statement

theorem Rat.det2_fib : ((x0 : AxNat) -> Eq.{1} Rat (Rat.det2 (Rat.ofInt (Int.ofNat (AxNat.fib (AxNat.succ (AxNat.succ x0))))) (Rat.ofInt (Int.ofNat (AxNat.fib (AxNat.succ x0)))) (Rat.ofInt (Int.ofNat (AxNat.fib (AxNat.succ x0)))) (Rat.ofInt (Int.ofNat (AxNat.fib x0)))) (Rat.ofInt (Int.pow (Int.neg Int.one) (AxNat.succ x0))))

Dependencies

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

4 direct dependencies 0 direct dependents

Evidence

kernel-Rat.det2_fib

Kind: kernel-term
Status: checked

Supports: `Rat.det2_fib` is admitted with exactly the type in `formal.statement` -- pinned verbatim by a committed test, `det2_fib_is_cassini_through_det2`, added specifically because (per that test's own doc comment) an empty axiom footprint on a theorem named `det2_fib` says nothing about which statement it proves, and this checks it is genuinely Cassini's identity read through `det2`, cast into ℚ by `ofInt`, and not some vacuous or mismatched restatement.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib rat_prelude::rat_prelude_tests::det2_fib_is_cassini_through_det2 -- --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. A deliberately misnamed test path exits 1.

footprint-Rat.det2_fib

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for Rat.det2_fib, verified as part of the same matrix-development sweep that verifies det2_mul.

Checker command

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

Evidence notes

Run 2026-08-24: exit 0. Same command against a misnamed test path exits 1.

dependencies-Rat.det2_fib

Kind: kernel-term
Status: checked

Supports: Rat.det2_fib's direct theorem dependencies, read from the proof term by Kernel::theorem_dependencies, are EXACTLY Int.fib_cassini, Rat.ofInt_add, Rat.ofInt_mul, Rat.ofInt_neg -- confirming the DERIVED-FROM-CASSINI claim in `statement` above and, just as importantly, confirming the ABSENCE of Rat.det2_mul from this fact's proof term. This is the load-bearing evidence for this lane's depends_on decision: det2_fib depends on Cassini directly (so this fact records `depends_on: [F:cassini-identity-over-constructed-integers]`) and does NOT depend on det2_mul, so a correspondence between Cassini and determinant-multiplicativity is not a `depends_on` edge in disguise.

Checker command

test "$(scripts/cargo-serialized.sh run --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- det2_fib 2>&1 | grep -Fc "Rat.det2_fib	Int.fib_cassini,Rat.ofInt_add,Rat.ofInt_mul,Rat.ofInt_neg")" -ge 1

Evidence notes

Run 2026-08-24: exit 0. A deliberately wrong substring run through the identical command exits 1.

Provenance

{
  "date": "2026-08-24",
  "established_by": "lane agent-correspondence-cassini (2026-08-24), closing ADR-0546's motivating example. Rat.det2_fib itself was proved by an earlier lane (see matrix.rs's module comment on the Fibonacci-determinant bridge); this lane's contribution is making the already-admitted theorem an addressable fact, tracing its actual (not classically-imagined) proof dependencies, and using it as the `via` step of X:cassini-specializes-determinant-multiplicativity.",
  "sources": [
    "crates/axeyum-lean-kernel/src/rat_prelude/matrix.rs",
    "crates/axeyum-lean-kernel/src/rat_prelude.rs",
    "crates/axeyum-lean-kernel/src/rat_prelude/rat_prelude_tests.rs",
    "artifacts/facts/F-cassini-identity-over-constructed-integers.json"
  ]
}