An exhausted pivot scan means the column is zero at every row it passed

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

Recorded description

For every matrix M : Nat -> Nat -> Rat, every column c, start index and row count rows, and every row q, IF Nat.Le start q and Nat.Lt q rows and Eq Nat (Rat.pivotSearch M c start rows) rows THEN Eq Rat (M q c) Rat.zero -- and the same for the fuelled Rat.pivotSearchAux under the extra hypothesis Nat.Lt q (Nat.add r fuel). This is the FIRST DISJUNCT of ADR-1554 obligation 2, which ADR-1562 recorded open and explained: it is a statement about every index the scan VISITED rather than about the one it returned, so the accumulated range has to sit in the motive, and F:rat-pivot-search-ne-zero (the value half) does not generalize to it. With the range half (F:rat-pivot-search-le-rows), the value half and this, obligation 2 is complete. The fuel bound is not removable for the same reason as in F:rat-clear-below-zero: a scan that runs out of fuel answers rows exactly as one that reached the bound does. Three of the four leaves are refutations and only one does work: the ble-true branch is refuted from Le r q and Lt q rows, and the isZeroB = false branch is refuted from its OWN hypothesis, because there the answer is r and Eq Nat r rows transports Lt r rows into Lt rows rows.

Formal statement

theorem Rat.pivotSearch_column_zero : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat.le x2 x4) -> ((x6 : AxNat.lt x4 x3) -> ((x7 : Eq.{1} AxNat (Rat.pivotSearch x0 x1 x2 x3) x3) -> Eq.{1} Rat (x0 x4 x1) Rat.zero)))))))) ; theorem Rat.pivotSearchAux_column_zero : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : AxNat.le x5 x3) -> ((x7 : AxNat.lt x3 x2) -> ((x8 : AxNat.lt x3 (AxNat.add x5 x4)) -> ((x9 : Eq.{1} AxNat (Rat.pivotSearchAux x0 x1 x2 x4 x5) x2) -> Eq.{1} Rat (x0 x3 x1) Rat.zero))))))))))

Dependencies

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

5 direct dependencies 1 direct dependents

Evidence

rat-pivot-search-column-zero-1

Kind: kernel-term
Status: checked

Supports: Both forms are checked, axiom-free theorems in all four rational preludes, populations pinned separately at four. Each regex pins the exhaustion hypothesis and the conclusion together: `Eq.{1} AxNat (Rat.pivotSearch x0 x1 x2 x3) x3` followed by `Eq.{1} Rat (x0 x4 x1) Rat.zero`, where `x4` is the ARBITRARY in-range row and `x1` the column searched. A version concluding about the START row `x2` would be strictly weaker, would not supply the loop invariant, and would not match.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^[a-z]+[[:space:]]+theorem[[:space:]]+Rat\.pivotSearch_column_zero[[:space:]]+0[[:space:]].*\(Rat\.pivotSearch x0 x1 x2 x3\) x3\) -> Eq\.\{1\} Rat \(x0 x4 x1\) Rat\.zero\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The hypothesis is shown SATISFIABLE and the conclusion OBSERVABLE at `[[0,1],[0,2]]`, where column 0 is all zero so the scan answers `rows` by reduction and the conclusion is checked at BOTH rows it passed. The control is the same matrix's column 1, where the scan lands on row 0, the hypothesis is unavailable, and the entries are nonzero -- so the conclusion would be FALSE there.

rat-pivot-search-column-zero-2

Kind: kernel-term
Status: checked

Supports: Both forms are checked, axiom-free theorems in all four rational preludes, populations pinned separately at four. Each regex pins the exhaustion hypothesis and the conclusion together: `Eq.{1} AxNat (Rat.pivotSearch x0 x1 x2 x3) x3` followed by `Eq.{1} Rat (x0 x4 x1) Rat.zero`, where `x4` is the ARBITRARY in-range row and `x1` the column searched. A version concluding about the START row `x2` would be strictly weaker, would not supply the loop invariant, and would not match.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^[a-z]+[[:space:]]+theorem[[:space:]]+Rat\.pivotSearchAux_column_zero[[:space:]]+0[[:space:]].*\(Rat\.pivotSearchAux x0 x1 x2 x4 x5\) x2\) -> Eq\.\{1\} Rat \(x0 x3 x1\) Rat\.zero\)\)\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The hypothesis is shown SATISFIABLE and the conclusion OBSERVABLE at `[[0,1],[0,2]]`, where column 0 is all zero so the scan answers `rows` by reduction and the conclusion is checked at BOTH rows it passed. The control is the same matrix's column 1, where the scan lands on row 0, the hypothesis is unavailable, and the entries are nonzero -- so the conclusion would be FALSE there.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/pivot_content.rs)",
  "source": "docs/research/09-decisions/adr-1571-obligation-3-closes-obligation-2-completes-and-obligation-4-is-four-lemmas-not-one.md"
}