A rational matrix with no rows has every column free

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

Recorded description

For every matrix M : Nat -> Nat -> Rat and every column count cols, Rat.nullity M 0 cols = cols. With no rows there is no pivot column, so every column is free and the nullity is the full width. The proof reads Rat.rank_nullity backwards through Rat.rankCols_zero_rows: rankCols M 0 cols + nullity M 0 cols = cols and rankCols M 0 cols = 0 give Nat.add 0 (nullity M 0 cols) = cols, and Nat.add recurses on its RIGHT argument, so Nat.zero_add is genuinely needed to strip the leading zero -- add 0 x is not x by reduction in this kernel. This is the DISCRIMINATING degenerate control for the pair: a Rat.nullity that returned 0 identically satisfies Rat.rankCols_zero_rows and Rat.nullity_zero_cols and fails this.

Formal statement

theorem Rat.nullity_zero_rows : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> Eq.{1} AxNat (Rat.nullity x0 AxNat.zero x1) x1))

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

rat-nullity-zero-rows-1

Kind: kernel-term
Status: checked

Supports: `Rat.nullity_zero_rows` is a checked `Declaration::Theorem` with an EMPTY axiom footprint in all four preludes, and its rendered type shows the row count instantiated at `AxNat.zero` with the answer being `x1` -- the column count itself, NOT zero. That distinction is the entire discriminating content: a `Rat.nullity` that returned `0` identically would still be admitted with the right type at every other degenerate lemma in the family, and would fail exactly here.

Checker command

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

Evidence notes

Run 2026-09-02: exactly four rows match name, kind, axiom count `0` and the rendered conclusion `Eq.{1} AxNat (Rat.nullity x0 AxNat.zero x1) x1`; the checker requires exactly 4. `scripts/new-fact.py` verified the pattern fails on mutated output. The anchor includes the literal `AxNat.zero` in argument position, so a version stated at a symbolic row count -- which would be FALSE -- does not match.

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