Rank-nullity over the rationals, in column form

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

Recorded description

For every matrix M : Nat -> Nat -> Rat and every pair of dimensions rows, cols, Nat.add (Rat.rankCols M rows cols) (Rat.nullity M rows cols) = cols. Rat.rankCols M rows cols is Nat.countRange (Rat.isPivotColB (Rat.rowEchelon M rows cols) rows cols) cols -- the number of columns j < cols such that some row r < rows of the row-echelon form has Rat.leadingIndex equal to j. Rat.nullity is the same count at Nat.setCompl of that predicate: the FREE columns. The theorem is one application of Nat.countRange_compl and is symbolic in all three arguments; nothing in its proof uses any property of Rat.rowEchelon, and it would hold verbatim if the elimination were the identity. That is deliberate: nullity is NOT defined as cols - rank, because the subtraction form inherits rank <= cols, which is open in this tree (ADR-1555) since it asserts the echelon form has at most one pivot per column -- ADR-1554 obligation 4. The column form relocates the whole obligation into the single bridge rank = rankCols, which is NOT proved here.

Formal statement

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

Dependencies

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

2 direct dependencies 4 direct dependents

Evidence

rat-rank-nullity-1

Kind: kernel-term
Status: checked

Supports: `Rat.rank_nullity` is a checked `Declaration::Theorem` with an EMPTY axiom footprint in all four preludes carrying the rationals, AND its admitted type renders with the conclusion `AxNat.add (Rat.rankCols x0 x1 x2) (Rat.nullity x0 x1 x2) = x2`. The checker greps the RENDERED TYPE and not only the name, so it fails not just on a deletion or a rename but on the statement changing while the name survives -- for instance a version bounding the sum by `x1` (the row count) instead of `x2`, which would be a different and false theorem.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>/dev/null | grep -cE '^(rat|creal|complex|cpoint)[[:space:]]+theorem[[:space:]]+Rat\.rank_nullity[[:space:]]+0[[:space:]].*AxNat\.add \(Rat\.rankCols x0 x1 x2\) \(Rat\.nullity x0 x1 x2\)\) x2\)\)\)$' 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^4$')" = 1

Evidence notes

Run 2026-09-02: the projection lists exactly four rows (rat, creal, complex, cpoint) matching name, kind `theorem`, axiom count `0` and the full rendered conclusion; the checker requires the count to be exactly 4 and exits 1 otherwise. `scripts/new-fact.py` verified the pattern fails on mutated output before this file was written. The anchor is the rendered CONCLUSION rather than the whole type because the binder prefix is shared by every three-argument matrix theorem in the family and would not discriminate.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/nullity.rs)",
  "source": "docs/research/09-decisions/adr-1558-rank-nullity-lands-in-column-form-and-the-bridge-to-the-row-form-is-the-open-obligation.md"
}