Row rank equals column rank over the rationals

Identifier: F:rat-rank-eq-rank-cols
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every matrix M : Nat -> Nat -> Rat and every rows, cols, Eq Nat (Rat.rank M rows cols) (Rat.rankCols M rows cols) -- UNCONDITIONALLY. Rat.rank counts the NONZERO ROWS of the row-echelon form over [0, rows); Rat.rankCols counts the PIVOT COLUMNS over [0, cols). ADR-1558 measured this as the open bridge; ADR-1562 discharged it modulo one hypothesis, the pivot section; ADR-1574 closed ADR-1554's obligation 4 and F:rat-pivot-section-of-is-echelon discharges the hypothesis. This is the statement whose two sides are counted over DIFFERENT index ranges, which is why it needs a cross-bound counting law rather than a reindexing, and ADR-1562's finding was that pointing that law at the COLUMNS as the left-hand count makes its injectivity hypothesis free while pointing it at the rows makes it the whole obligation.

Formal statement

theorem Rat.rank_eq_rankCols : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (Rat.rank x0 x1 x2) (Rat.rankCols x0 x1 x2))))

Dependencies

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

2 direct dependencies 2 direct dependents

Evidence

rat-rank-eq-rank-cols-1

Kind: kernel-term
Status: checked

Supports: A checked, axiom-free theorem in all four rational preludes, population pinned at four. The regex requires the type to have NO hypothesis between the three binders and the conclusion, which is the whole difference from F:rat-rank-eq-rank-cols-of-pivot-section: it pins the conclusion immediately after `(x2 : AxNat) ->` with the closers of exactly three binders, so the conditional form does not match. It also pins the axiom-footprint column at 0.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^[a-z]+[[:space:]]+theorem[[:space:]]+Rat\.rank_eq_rankCols[[:space:]]+0[[:space:]].*Eq\.\{1\} AxNat \(Rat\.rank x0 x1 x2\) \(Rat\.rankCols x0 x1 x2\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows, mutation-checked by `scripts/new-fact.py`. The registered evaluation test in `rat_prelude/echelon_section_tests.rs` reduces `Rat.rank` and `Rat.rankCols` at `[[1,2],[2,4]]` (both 1) and `[[0,1],[2,3]]` (both 2, and the reduction needs the pivot swap), each against a hand-computed numeral with a control that must NOT be `def_eq` -- so a `rank` that always answered `rows`, or always `0`, fails one of the pair. The theorem is then applied at fully free arguments with no hypothesis.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/echelon_section.rs)",
  "source": "docs/research/09-decisions/adr-1574-obligation-4-closes-and-the-exit-derivation-folds-into-the-induction.md"
}