The rank of a rational matrix is at most its row count

Identifier: F:rat-rank-le-rows
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.Le (Rat.rank M rows cols) rows. Rat.rank M rows cols is Nat.countRange (Rat.nonzeroRowB (Rat.rowEchelon M rows cols) cols) rows -- the number of rows of the row-echelon form whose Rat.leadingIndex is strictly below cols, i.e. the number of nonzero rows. The bound follows from Nat.countRange_le alone and uses NO property of Rat.rowEchelon, of Rat.leadingIndex, or of the elementary row operations: a count of any predicate over the range [0, rows) cannot exceed rows. That is why this half of the dimension bound is free, and why the other half (rank <= cols) is not -- rank <= cols asserts that the echelon form has at most one pivot per column, which is the unproved rowEchelon_isEchelon (ADR-1554 obligation 4).

Formal statement

theorem Rat.rank_le_rows : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> AxNat.le (Rat.rank x0 x1 x2) x1)))

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

rat-rank-le-rows-1

Kind: kernel-term
Status: checked

Supports: `Rat.rank_le_rows` is a checked `Declaration::Theorem` with an EMPTY `Kernel::axiom_footprint` in all four preludes carrying the rationals. The `formal.statement` is the kernel's `render_lean` of the admitted type; reading it confirms the bound is against the FIRST dimension argument `x1` (the row count) and not against `x2`, which is the whole content of the claim -- the same declaration bounding rank by `x2` would be `rank_le_cols`, which is not proved here.

Checker command

out=$(target/release/examples/kernel_declaration_projection --require-declaration Rat.rank_le_rows --require-kind theorem 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'found[[:space:]]+(rat|creal|complex|cpoint)[[:space:]]+theorem[[:space:]]+Rat\.rank_le_rows[[:space:]]+0$')" = 4

Evidence notes

Run 2026-09-02: prints four `found ... theorem Rat.rank_le_rows 0` rows (rat, creal, complex, cpoint) and exits 0. The checker COUNTS those rows and requires exactly 4, so a deletion, a rename, a demotion to a `Definition`, a nonzero axiom footprint, or the declaration failing to survive into a downstream prelude each make the count differ and the command exit 1. `scripts/new-fact.py` verified the pattern fails on mutated output before this file was written.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/rank.rs)",
  "source": "docs/research/09-decisions/adr-1555-rank-is-an-uncapped-count-and-row-operation-invariance-does-not-follow-from-the-inverse-laws.md"
}