Rank-nullity over the rationals, in the row form

Identifier: F:rat-rank-nullity-rows
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 (Nat.add (Rat.rank M rows cols) (Rat.nullity M rows cols)) cols -- UNCONDITIONALLY. ADR-1558 landed rank-nullity in the COLUMN form (F:rat-rank-nullity, rankCols + nullity = cols), which is a partition of the column range and needs nothing about echelon form; the ROW form is that theorem with rankCols rewritten to rank across F:rat-rank-eq-rank-cols and nothing else. The two forms are genuinely different statements: rank counts nonzero ROWS of the reduced matrix and rankCols counts pivot COLUMNS, and identifying them is the content of the bridge.

Formal statement

theorem Rat.rank_nullity_rows : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (AxNat.add (Rat.rank x0 x1 x2) (Rat.nullity x0 x1 x2)) x2)))

Dependencies

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

3 direct dependencies 0 direct dependents

Evidence

rat-rank-nullity-rows-1

Kind: kernel-term
Status: checked

Supports: A checked, axiom-free theorem in all four rational preludes, population pinned at four. The regex pins the LEFT summand as `Rat.rank` and not `Rat.rankCols` -- the column form F:rat-rank-nullity was already free and is a different statement -- and requires no hypothesis binder. 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_nullity_rows[[:space:]]+0[[:space:]].*Eq\.\{1\} AxNat \(AxNat\.add \(Rat\.rank x0 x1 x2\) \(Rat\.nullity x0 x1 x2\)\) x2\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows, mutation-checked by `scripts/new-fact.py`. Checked AT THE NUMBERS as well as symbolically in `rat_prelude/echelon_section_tests.rs`: `rank + nullity` reduces to the column count at `[[1,2],[2,4]]` (1 + 1) and at `[[0,1],[2,3]]` (2 + 0), and the free-variable application carries a control refusing the column form.

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"
}