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

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

Recorded description

For every matrix M : Nat -> Nat -> Rat and every rows, cols, Nat.Le (Rat.rank M rows cols) cols -- UNCONDITIONALLY. ADR-1555 recorded this as open and explained why it is not free the way Nat.Le (Rat.rank M rows cols) rows is: rank is an UNCAPPED count of nonzero rows over [0, rows), so the row bound is immediate from the counting range while the column bound is a statement about the echelon form. It is transported from the free bound on Rat.rankCols across F:rat-rank-eq-rank-cols.

Formal statement

theorem Rat.rank_le_cols : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> AxNat.le (Rat.rank 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-le-cols-1

Kind: kernel-term
Status: checked

Supports: A checked, axiom-free theorem in all four rational preludes, population pinned at four. The regex pins `AxNat.le (Rat.rank x0 x1 x2) x2` -- the bound against the COLUMN count `x2` and not the row count `x1`, which is F:rat-rank-le-rows and was already free -- and requires no hypothesis binder, which is the difference from F:rat-rank-le-cols-of-pivot-section.

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_le_cols[[:space:]]+0[[:space:]].*AxNat\.le \(Rat\.rank x0 x1 x2\) x2\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows, mutation-checked by `scripts/new-fact.py`. The registered test applies it at free arguments and carries an explicit control refusing the ROW bound, because the two differ by one variable and the row bound is the easy one.

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