Rat.det_transpose: the determinant is invariant under transpose, at symbolic dimension

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

Recorded description

For every dimension n and every matrix A (a function Nat -> Nat -> Rat plus an explicit bound), det (matTranspose A) n = det A n. The dimension is symbolic and the matrix universally quantified, so this is the general law and not a fixed-dimension instance. It is the THIRD of the four laws ADR-1120 named over the general-n determinant, after det matId n = 1 (ADR-1135) and general-row expansion (ADR-1185); only multiplicativity remains, and ADR-1135 established that it is blocked on an aggregate type this kernel does not have rather than on effort. The proof is one induction on the dimension with the matrix under the motive. Rat.det_succ expands det (matTranspose A) (succ m) along the transpose's first row, whose entries are A's first COLUMN -- matTranspose A 0 q reduces to A q 0 by delta and beta alone. Under Rat.sumRange_congr, Rat.matMinor_transpose (an Eq.refl, since both sides reduce to A (matSkip q c) (matSkip 0 r)) plus Rat.det_congr rewrite each minor of the transpose into the transpose of a minor, which the induction hypothesis strips. What remains is expansion along A's first column, and Rat.det_col_expansion closes it.

Formal statement

theorem Rat.det_transpose : ((x0 : AxNat) -> ((x1 : ((x1 : AxNat) -> ((x2 : AxNat) -> Rat))) -> Eq.{1} Rat (Rat.det (Rat.matTranspose x1) x0) (Rat.det x1 x0)))

Dependencies

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

3 direct dependencies 0 direct dependents

Evidence

kernel-Rat.det_transpose

Kind: kernel-term
Status: checked

Supports: Rat.det_transpose 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_transpose 2>/dev/null | grep -cE '^Rat\.det_transpose[[: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 -- GNU grep reads \t as a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. Pass ONE name per invocation: this tool silently consumes only its FIRST name argument. --release is MANDATORY; in debug the example SIGABRTs on a stack overflow, which reads like an absent declaration.

footprint-Rat.det_transpose

Kind: exhaustive-enumeration
Status: checked

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

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.

control-det-transpose-is-not-vacuous

Kind: kernel-term
Status: checked

Supports: det (matTranspose A) 3 evaluates to 13 on a pinned 3x3 whose determinant Rat.det_eval_example independently pins at 13, and the SAME test first asserts that matTranspose A 0 1 is 0 and is NOT 2 = A 0 1, so the matrix is genuinely moved by the transpose. The admitted theorem is then APPLIED at n = 3 and its inferred type compared against the statement rebuilt independently in the test.

Checker command

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

Evidence notes

The count is tested, not just the exit status: `1 passed` fails if the test is renamed away or filtered out. The non-symmetry assertion is the check without which this whole cluster would be vacuous -- for a symmetric A, matTranspose A is A and det Aᵀ = det A says nothing. The Rat.matMinor_transpose pins use matMinor Aᵀ 0 2 = [[2,1],[0,3]] rather than matMinor Aᵀ 0 1 = [[2,0],[0,1]], because the latter is symmetric and would not separate a transposed index.

control-adr-1210-numeric-sweep

Kind: exhaustive-enumeration
Status: checked

Supports: det (transpose A) n = det A n over 360 random matrices at n = 0..5, with the induction step's every claim re-derived: the minor identification over 7,000 index pairs, the double-minor agreement over 5,310, and the sign identity over 144 index pairs.

Checker command

python3 docs/research/09-decisions/adr-1210-det-transpose-checks.py

Evidence notes

Simulates Rat.matSkip, Rat.matMinor, Rat.altSign, Rat.det and Rat.matTranspose over Fraction at exactly the definitions rat_prelude/matrix_det.rs uses, and exits 1 if any claim fails. Section 0 checks the transcription itself against a Leibniz determinant, so a wrong simulation cannot silently agree with a wrong proof, and section 8 confirms the sampled matrices are not accidentally symmetric. Section 9 measures the claim ADR-1185 made and this ADR corrects: the row law holds, and each column summand is the c = 0 slice of a row expansion, which is why the row law cannot supply the column sum.

control-det-transpose-mutation

Kind: exhaustive-enumeration
Status: checked

Supports: Under the Rat.matSkip branch-swap mutation the statement is FALSE at 229 of 240 instances and the declaration is refused. Under the column-entry-index mutation the declaration is also refused, but the STATEMENT stays true -- recorded as a broken proof rather than a false theorem, because a rejection with a true statement adds no coverage.

Checker command

python3 docs/research/09-decisions/adr-1210-det-transpose-checks.py 2>&1 | grep -cE '^     det_transpose +FALSE'

Evidence notes

grep -c on a tested count, consuming the whole pipe. The declaration column was measured once in an isolated worktree with declare_matrix_det rewritten to REPORT each rejection instead of short-circuiting, and is recorded in ADR-1210's table rather than re-run here. Under the matSkip mutation four of this lane's five declarations report UnknownConst, confounded by Rat.matSkip_succ_succ failing upstream -- which is why a second, statement-shaped mutation was designed, and it refuses exactly the two declarations that mention the column summand and no others.

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 det-transpose. Design note: ADR-1210."
}