The column rank is at most the row rank, with no hypothesis

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

Recorded description

For every matrix M over the constructed rationals and all dimensions rows and cols, Rat.rankCols M rows cols is at most Rat.rank M rows cols. UNCONDITIONALLY: no section hypothesis and no echelon-form obligation. F:rat-rank-eq-rank-cols-of-pivot-section gives the two counts as EQUAL but has to assume the section hypothesis, because the cross-bound counting law it goes through needs a constructive inverse; the inequality in this direction needs only the injection, and the two hypotheses that costs are exactly the two the bridge already discharges from its two searches.

Formal statement

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

Dependencies

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

5 direct dependencies 0 direct dependents

Evidence

kernel-rat-rank-cols-le-rank

Kind: kernel-term
Status: checked

Supports: Rat.rankCols_le_rank is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>&1) && test "$(printf "%s\n" "$out" | grep -cF -e '-> AxNat.le (Rat.rankCols x0 x1 x2) (Rat.rank x0 x1 x2))))')" -ge 1

Evidence notes

The pattern is a DISTINGUISHING substring of the admitted type, not the declaration's name: an existence check would still pass if the statement drifted. Verified to hit ZERO on a perturbed pattern before this row was written -- see the mutation table in ADR-1593. `kernel_declaration_projection` prints every declaration with its footprint size and its rendered type, and the prelude build admits this theorem only through the trusted gate, so a successful build IS the type-check. `grep -cF -e` rather than `grep -cF`: a pattern beginning with `-` is parsed as an OPTION, and five of these seven do. The table in ADR-1593 caught that -- the rows failed as written before `-e` was added, which is why it was run at all.

footprint-rat-rank-cols-le-rank

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- read from Kernel::axiom_footprint for this declaration, not from a maintained list

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>&1) && test "$(printf "%s\n" "$out" | awk -F'\t' '$3 == "Rat.rankCols_le_rank" && $4 == "0"' | wc -l)" -ge 1

Evidence notes

The pattern pins BOTH the declaration name and the footprint size 0, so a proof that reached for a trusted declaration would fail the check rather than be reported as axiom-free. A one-character name typo hits zero rows, and so does asking for any size other than 0.

statement-rat-rank-cols-le-rank

Kind: instance-pin
Status: checked

Supports: The statement says what its name says -- checked at a concrete instance with hand-computed numerals and paired with the specific wrong statement it rules out

Checker command

cargo test -q --release -p axeyum-lean-kernel --lib -- rat_prelude::rank_bridge_tests --test-threads=4

Evidence notes

A `rankCols_le_rank` that had quietly kept the section hypothesis would still be called that and would still be admitted. `rat_prelude/rank_bridge_tests.rs` reads the declared type out of the environment and forbids `Rat.nonzeroRowB` (the section hypothesis cannot be stated without it) and the transposed bound (a different theorem, and one that is NOT free -- in that orientation the injectivity obligation is ADR-1554 obligation 4).

Provenance

{
  "date": "2026-09-03",
  "established_by": "axeyum-lean-kernel build_nat_prelude",
  "source": "declaration name and canonical type read directly from kernel_declaration_projection, which prints render_lean of the admitted type; lane finset-pigeonhole, ADR-1593."
}