Rat.det_eq_det2: the general-n determinant agrees with the fixed 2x2 one, symbolically in the matrix

Identifier: F:rat-det-general-n-eq-det2
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Rat.det is the determinant over the constructed rationals at GENERAL n -- the dimension is an argument, not a fixed arity -- defined by cofactor expansion along the first row: det A 0 = 1 and det A (n+1) = sum over j < n+1 of altSign j * (A 0 j * det (matMinor A 0 j) n). A matrix is a function Nat -> Nat -> Rat plus an explicit bound (this kernel has no List, Finset, Prod or vector type), and the minor is the index reindex matMinor A i j r c = A (matSkip i r) (matSkip j c) with matSkip p x = if p <= x then x+1 else x. This fact records that det A 2 equals Rat.det2 (A 0 0) (A 0 1) (A 1 0) (A 1 1) for EVERY matrix A -- a universally quantified agreement, not an evaluation at one matrix. Rat.det2 was declared independently of this construction, so the agreement is the strongest available check that the cofactor recursion means what it says: it pins the minor's index shift and the alternating sign at once. What it does NOT establish is any property of det at symbolic n -- multiplicativity, transpose invariance, expansion along a general row, and det matId n = 1 are all unproved.

Formal statement

theorem Rat.det_eq_det2 : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> Eq.{1} Rat (Rat.det x0 (AxNat.succ (AxNat.succ AxNat.zero))) (Rat.det2 (x0 AxNat.zero AxNat.zero) (x0 AxNat.zero (AxNat.succ AxNat.zero)) (x0 (AxNat.succ AxNat.zero) AxNat.zero) (x0 (AxNat.succ AxNat.zero) (AxNat.succ AxNat.zero))))

Dependencies

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

4 direct dependencies 5 direct dependents

Evidence

kernel-Rat.det_eq_det2

Kind: kernel-term
Status: checked

Supports: Rat.det_eq_det2 is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- Rat.det_eq_det2 2>/dev/null | grep -cE '^Rat\\.det_eq_det2[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. Pass ONE name per invocation: this tool consumes only its first name argument and silently discards the rest. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-Rat.det_eq_det2

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the rat prelude's trusted surface is empty, which bounds Rat.det_eq_det2.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free rat

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty rat surface bounds every declaration in it. The per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

suite-det-eq-det2

Kind: kernel-term
Status: checked

Supports: The determinant family is a checked Definition/Theorem with an empty axiom footprint, read out of kernel.environment() rather than off the diff, and the evaluation examples reject a deliberately wrong value.

Checker command

cargo test -p axeyum-lean-kernel --lib determinant 2>&1 | grep -cE '^test result: ok\. 3 passed'

Evidence notes

The count is tested, not just the exit status: `3 passed` fails if a test is renamed away or silently filtered out, which a bare `cargo test <filter>` cannot detect (a filter matching nothing prints 'running 0 tests ... ok' and exits 0). Mutation-verified twice on 2026-08-31 in this lane's worktree, each mutation restored afterwards and `git diff` confirmed empty: (a) swapping Rat.matSkip's two branches made build_rat_prelude fail with DeclarationValueMismatch at Rat.det_eq_det2; (b) changing det_eval_example's stated value from 13 to 12 made it fail with DeclarationValueMismatch. So both the agreement theorems and the evaluation examples are load-bearing rather than decorative.

Provenance

{
  "date": "2026-08-31",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/matrix_det.rs)",
  "source": "Lane general-n-determinant, against ADR-1075's depth proposal naming the determinant at general n as linear algebra's keystone."
}