A pivot found in range is at or below where the search started

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

Recorded description

For every matrix M : Nat -> Nat -> Rat, every column c, row count rows and starting row start, IF Nat.Lt (Rat.pivotSearch M c start rows) rows THEN Nat.Le start (Rat.pivotSearch M c start rows), and likewise for the fuelled form Rat.pivotSearchAux at every fuel. In words: when the pivot scan lands in range, it lands at or below the row it started from. THE HYPOTHESIS IS NOT DECORATION: both exhaustion routes of the scan answer rows, and rows is not >= start when the scan was started past the row count, so the unconditional statement is false. ADR-1558 landed the other side of this bound (F:rat-pivot-search-le-rows, which needs no hypothesis because rows satisfies it); together they pin the found pivot to the half-open interval [start, rows), which is exactly what F:rat-row-swap-preserves-zero-range and F:rat-clear-below-row-swap-off both require of the row the pivot step swaps in.

Formal statement

theorem Rat.pivotSearch_ge_start : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat.lt (Rat.pivotSearch x0 x1 x2 x3) x3) -> AxNat.le x2 (Rat.pivotSearch x0 x1 x2 x3)))))) ; theorem Rat.pivotSearchAux_ge_start : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat.lt (Rat.pivotSearchAux x0 x1 x2 x3 x4) x2) -> AxNat.le x4 (Rat.pivotSearchAux x0 x1 x2 x3 x4)))))))

Dependencies

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

4 direct dependencies 1 direct dependents

Evidence

rat-pivot-search-ge-start-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 is anchored on the DIRECTION of the bound -- `AxNat.le <start> (Rat.pivotSearch …)`, the search term on the RIGHT -- so it cannot be satisfied by F:rat-pivot-search-le-rows's statement, which is the bound the other way round and was already landed. It also pins the axiom-footprint column at 0.

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

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. Spent exactly twice, both in `echelonAux`'s pivot branch: it is what makes `Rat.rowSwap_preserves_zero_range` and `Rat.clearBelow_rowSwap_off` applicable, since both need the row the swap brings in to be at or below the cursor. Those two lemmas' own registered tests exhibit a matrix where the conclusion is FALSE when that bound is dropped, which is the evidence that this statement is doing work rather than restating a bound already present.

rat-pivot-search-ge-start-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 is anchored on the DIRECTION of the bound -- `AxNat.le <start> (Rat.pivotSearch …)`, the search term on the RIGHT -- so it cannot be satisfied by F:rat-pivot-search-le-rows's statement, which is the bound the other way round and was already landed. It also pins the axiom-footprint column at 0.

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

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. Spent exactly twice, both in `echelonAux`'s pivot branch: it is what makes `Rat.rowSwap_preserves_zero_range` and `Rat.clearBelow_rowSwap_off` applicable, since both need the row the swap brings in to be at or below the cursor. Those two lemmas' own registered tests exhibit a matrix where the conclusion is FALSE when that bound is dropped, which is the evidence that this statement is doing work rather than restating a bound already present.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/echelon_invariant.rs)",
  "source": "docs/research/09-decisions/adr-1574-obligation-4-closes-and-the-exit-derivation-folds-into-the-induction.md"
}