Rat.det_congr: the general-n determinant respects pointwise equality of matrices

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

Recorded description

Rat.det is the determinant over the constructed rationals at GENERAL n, by cofactor expansion along the first row, over matrices encoded as functions Nat -> Nat -> Rat plus an explicit bound (F:rat-det-general-n-eq-det2 records the construction). This fact records that if two matrices agree at every index pair -- for all r and c, A r c = B r c -- then det A n = det B n, for every n. The hypothesis is POINTWISE and cannot be strengthened to an equation between the two matrices, because this kernel has no funext; the unhypothesized form is false. This is the lemma that unblocks induction over the dimension: det's recursive call is at the MINOR, so any such induction arrives at a matrix that is only pointwise the one the induction hypothesis is about.

Formal statement

theorem Rat.det_congr : ((x0 : AxNat) -> ((x1 : ((x1 : AxNat) -> ((x2 : AxNat) -> Rat))) -> ((x2 : ((x2 : AxNat) -> ((x3 : AxNat) -> Rat))) -> ((x3 : ((x3 : AxNat) -> ((x4 : AxNat) -> Eq.{1} Rat (x1 x3 x4) (x2 x3 x4)))) -> Eq.{1} Rat (Rat.det x1 x0) (Rat.det x2 x0)))))

Dependencies

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

2 direct dependencies 4 direct dependents

Evidence

kernel-Rat.det_congr

Kind: kernel-term
Status: checked

Supports: Rat.det_congr 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_congr 2>/dev/null | grep -cE '^Rat\.det_congr[[: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. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. Pass ONE name per invocation. --release is MANDATORY.

footprint-Rat.det_congr

Kind: exhaustive-enumeration
Status: checked

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

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.

suite-det-congr-hypothesis

Kind: kernel-term
Status: checked

Supports: The statement still carries its pointwise hypothesis, and det genuinely depends on its matrix argument -- so the hypothesis is not discardable.

Checker command

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

Evidence notes

The count is tested, not just the exit status: `2 passed` fails if a test is renamed away or silently filtered out. The shape pin asserts the rendered type still applies the first matrix to two indices, which only happens inside the pointwise premise -- a statement that lost the premise would match neither. The non-vacuity control is that det (matMinor matId 0 1) 2 is NOT def_eq to Rat.one while det matId 3 is: two matrices built by the same machinery whose determinants differ, so det does not ignore its matrix argument and det_congr is not the trivially-true statement it would be if it did.

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 determinant-laws, against ADR-1120's four open laws over the general-n determinant. Design note: ADR-1135."
}