Gaussian elimination's pivot search never returns an out-of-range row

Identifier: F:rat-pivot-search-le-rows
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every matrix M : Nat -> Nat -> Rat, every column c, every start index and every row count rows, Nat.Le (Rat.pivotSearch M c start rows) rows -- and the same bound for the fuelled Rat.pivotSearchAux at an arbitrary fuel and start. No bound on start is required: a start already past rows takes the out-of-range branch on its first step and returns rows. This is the RANGE HALF of ADR-1554 obligation 2, the postcondition of Rat.pivotSearch. That obligation is stated as a disjunction -- the answer is rows and column c is zero throughout [start, rows), or it is in [start, rows) with a nonzero entry there -- and both disjuncts assert result <= rows, which needs neither the Or nor the bounded forall. The content half, which of the two disjuncts holds, is NOT proved here and still needs the same fuel induction carrying an Or in its motive. The route is induction on the fuel with the row index generalised inside the motive, because the step instantiates its hypothesis at succ r rather than at r.

Formal statement

theorem Rat.pivotSearch_le_rows : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> AxNat.le (Rat.pivotSearch x0 x1 x2 x3) x3)))) ; theorem Rat.pivotSearchAux_le_rows : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> AxNat.le (Rat.pivotSearchAux x0 x1 x2 x3 x4) x2)))))

Dependencies

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

0 direct dependencies 4 direct dependents

Evidence

rat-pivot-search-le-rows-1

Kind: kernel-term
Status: checked

Supports: Both `Rat.pivotSearch_le_rows` and the fuelled `Rat.pivotSearchAux_le_rows` are checked `Declaration::Theorem`s with EMPTY axiom footprints in all four preludes, and both rendered types bound the search result by the ROW COUNT argument. The checker counts EIGHT rows (two declarations across four preludes) and requires exactly that, so losing either half -- or either half's statement drifting to a different bound -- makes the count differ and the command exit 1.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>/dev/null | grep -cE '^(rat|creal|complex|cpoint)[[:space:]]+theorem[[:space:]]+Rat\.pivotSearch(Aux)?_le_rows[[:space:]]+0[[:space:]].*AxNat\.le \(Rat\.pivotSearch(Aux)? x0 x1 x2 x3( x4)?\) x[23]\)+$' 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^8$')" = 1

Evidence notes

Run 2026-09-02: exactly eight rows match. `scripts/new-fact.py` verified the pattern fails on mutated output. The regex admits both arities deliberately (`pivotSearch` takes four arguments, `pivotSearchAux` five) and pins the bound to `x3` and `x2` respectively, which are the row-count binders in each signature -- so a version bounding by the column index would not match.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/pivot_bound.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"
}