The selection lemma over the constructed rationals: reindexing a matrix's rows by a self-map of [0,n) multiplies its determinant by the permutation matrix's

Identifier: F:rat-det-row-selection
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural m, every matrix B : Nat -> Nat -> Rat and every index map g : Nat -> Nat that sends [0, m+1) into itself (Nat.mapsInto g (m+1)), the determinant of B with its rows reindexed by g factors as det (fun r c => B (g r) c) (m+1) = det (fun r c => matId (g r) c) (m+1) * det B (m+1), where Rat.det is the general-n cofactor determinant and Rat.matId is the identity matrix. The MapsInto hypothesis cannot be dropped: at m = 0 with g 0 = 5 and B 5 0 = 7 the left side is 7 and the right side is matId 5 0 * det B 1 = 0. Proved constructively: Nat.injective_on_or_duplicate splits g into the injective case (a cursor induction over how many trailing positions g already fixes, using the finite pigeonhole principle, composition with Nat.transposition, and Rat.det_row_swap to pay for each move with one sign) and the case with an explicit duplicate pair (both determinants vanish by Rat.det_alternating). This is the second of the two obligations that determinant multiplicativity det (A*B) n = det A n * det B n at symbolic n reduces to.

Formal statement

theorem Rat.det_row_selection : ((x0 : AxNat) -> ((x1 : ((x1 : AxNat) -> ((x2 : AxNat) -> Rat))) -> ((x2 : ((x2 : AxNat) -> AxNat)) -> ((x3 : AxNat.mapsInto x2 (AxNat.succ x0)) -> Eq.{1} Rat (Rat.det (fun (x4 : AxNat) => fun (x5 : AxNat) => x1 (x2 x4) x5) (AxNat.succ x0)) (Rat.mul (Rat.det (fun (x4 : AxNat) => fun (x5 : AxNat) => Rat.matId (x2 x4) x5) (AxNat.succ x0)) (Rat.det x1 (AxNat.succ x0)))))))

Dependencies

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

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

Evidence

kernel-Rat.det_row_selection

Kind: kernel-term
Status: checked

Supports: `Rat.det_row_selection` is in the environment as a checked `Declaration::Theorem` (not a `Definition`, not an axiom) with an EMPTY `Kernel::axiom_footprint`, and the row printed carries the declaration kind and the footprint size so a change to either fails the check. The `formal.statement` above is the row's own `canonical_type` field, i.e. `Kernel::render_lean` of the admitted type -- not a paraphrase of the Rust source or of a doc comment.

Checker command

scripts/cargo-serialized.sh run --release -q -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration Rat.det_row_selection --require-kind theorem

Evidence notes

Run 2026-09-02: prints `found\trat\ttheorem\tRat.det_row_selection\t0` and exits 0. `--require-declaration` exits 1 with a message on stderr when NO prelude has a declaration with that exact display name, and `--require-kind theorem` additionally refuses a match of any other kind, so a deletion, a rename, or a demotion to a `Definition` each fail. `--release` is mandatory for this binary (it builds `creal`/`complex`/`cpoint`).

suite-Rat.det_row_selection

Kind: kernel-term
Status: checked

Supports: `rat_prelude_tests::the_determinant_toolkit_is_axiom_free` names `det_row_selection` in its targeted list and requires it to be a `Declaration::Theorem` with an empty axiom footprint, read from `kernel.environment()`. It is a second, independent route to the same two properties, and it fails as a build failure rather than as a missing row if the prelude stops admitting the declaration at all.

Checker command

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

Evidence notes

Run 2026-09-02: `test result: ok. 1 passed; 0 failed`. This row does NOT pin the statement -- the row above does that -- and on its own it could not distinguish this theorem from any other axiom-free theorem of the same name.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/matrix_det_mul.rs)",
  "source": "Lane det-mul-general-n, closing ADR-1440's obligation 2 (the selection lemma) on the way to determinant multiplicativity at symbolic n. Status note: docs/plan/status/det-mul-general-n.md."
}