Gaussian elimination's clearing sweep leaves the pivot row and everything above it untouched

Identifier: F:rat-clear-below-off
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every matrix M : Nat -> Nat -> Rat, every pivot row pr, pivot column pc, row count rows, row q and column c, IF Nat.Le q pr THEN Eq Rat (Rat.clearBelow M pr pc rows q c) (M q c) -- and the same for the fuelled Rat.clearBelowAux at an arbitrary fuel and cursor, under Nat.Lt q r. In words: a row at or above the pivot row is byte-for-byte what it was, at EVERY column. This is the 'rows outside that range are untouched' half of ADR-1554 obligation 3. It is not a convenience: the ZERO half's own proof consumes it, because when the sweep reaches the target row it rewrites that row once and then keeps recursing STRICTLY BELOW, so the value the caller asked about is fixed by rows the loop has not visited yet. The statement is unconditional in the FUEL, unlike F:rat-clear-below-zero: a row above the cursor is untouched whether the loop finishes or gives up, which is why the two halves are separate inductions rather than one conjunction.

Formal statement

theorem Rat.clearBelow_off : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : AxNat.le x4 x1) -> Eq.{1} Rat (Rat.clearBelow x0 x1 x2 x3 x4 x5) (x0 x4 x5)))))))) ; theorem Rat.clearBelowAux_off : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : ((x6 : AxNat) -> ((x7 : AxNat) -> Rat))) -> ((x7 : AxNat) -> ((x8 : AxNat.lt x3 x7) -> Eq.{1} Rat (Rat.clearBelowAux x0 x1 x2 x5 x6 x7 x3 x4) (x6 x3 x4))))))))))

Dependencies

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

1 direct dependencies 4 direct dependents

Evidence

rat-clear-below-off-1

Kind: kernel-term
Status: checked

Supports: Both the wrapper and the fuelled form are checked, axiom-free theorems in all four rational preludes, and the checker pins each population at four rows SEPARATELY, so losing either half is caught (a single combined count would pass on eight rows of one of them). Each regex is anchored on its own conclusion: the wrapper equates `Rat.clearBelow x0 x1 x2 x3 x4 x5` with `x0 x4 x5`, i.e. the swept entry with the ORIGINAL entry at the same (row, column) -- a version equating it with the entry at a different index, or with `Rat.zero`, 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\.clearBelow_off[[:space:]]+0[[:space:]].*-> Eq\.\{1\} Rat \(Rat\.clearBelow x0 x1 x2 x3 x4 x5\) \(x0 x4 x5\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The column argument is universally quantified and appears on both sides, which is what makes this the EVERY-column statement rather than the pivot-column one; the statement pin in `clear_below_tests.rs` additionally asserts the hypothesis is `AxNat.le x4 x1` and not `AxNat.lt x4 x1`, because the pivot row itself is untouched.

rat-clear-below-off-2

Kind: kernel-term
Status: checked

Supports: Both the wrapper and the fuelled form are checked, axiom-free theorems in all four rational preludes, and the checker pins each population at four rows SEPARATELY, so losing either half is caught (a single combined count would pass on eight rows of one of them). Each regex is anchored on its own conclusion: the wrapper equates `Rat.clearBelow x0 x1 x2 x3 x4 x5` with `x0 x4 x5`, i.e. the swept entry with the ORIGINAL entry at the same (row, column) -- a version equating it with the entry at a different index, or with `Rat.zero`, 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\.clearBelowAux_off[[:space:]]+0[[:space:]].*-> Eq\.\{1\} Rat \(Rat\.clearBelowAux x0 x1 x2 x5 x6 x7 x3 x4\) \(x6 x3 x4\)\)\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The column argument is universally quantified and appears on both sides, which is what makes this the EVERY-column statement rather than the pivot-column one; the statement pin in `clear_below_tests.rs` additionally asserts the hypothesis is `AxNat.le x4 x1` and not `AxNat.lt x4 x1`, because the pivot row itself is untouched.

Provenance

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