Gaussian elimination lands in row-echelon form

Identifier: F:rat-row-echelon-is-echelon
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every matrix M : Nat -> Nat -> Rat and every rows, cols, Rat.isEchelon (Rat.rowEchelon M rows cols) rows cols is true -- UNCONDITIONALLY, with no hypothesis on M or on the dimensions. This is ADR-1554's obligation 4, which ADR-1554 itself sized as 'at least a lane on its own and probably two' and ADR-1571 section 3 re-sized from measurement as four prerequisite lemmas plus an invariant plus two inductions. The loop form is also established: for every starting matrix and cursors, Rat.echelonAux rows cols fuel M pr pc lands in echelon form given five clauses -- the column cursor is in range (Nat.Le pc cols), the rows already placed pass the adjacent-pair test, they all lead strictly left of the column cursor, every row at or below the row cursor is zero everywhere left of the column cursor, and Nat.Le cols (Nat.add pc fuel). THE EXIT DERIVATION IS FOLDED INTO THE INDUCTION rather than run after it: the conclusion carried at every fuel level is already the answer, so each of the three leaves that stop the loop discharges it from the invariant and nothing ever has to name the final cursors -- which is why this is one induction and not the two ADR-1571 predicted. Two of those leaves share one derivation because Nat.add recurses on its right argument, so Nat.Le cols (Nat.add pc 0) IS Nat.Le cols pc; writing the fuel clause as pc + fuel rather than fuel + pc is what makes that identity definitional. The entry point needs no hypothesis because rowEchelon starts both cursors at 0, where three clauses are vacuous (Nat.Lt _ 0 has no inhabitant), one is Nat.zero_le and the last is one Nat.zero_add.

Formal statement

theorem Rat.rowEchelon_isEchelon : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} Bool (Rat.isEchelon (Rat.rowEchelon x0 x1 x2) x1 x2) Bool.true))) ; theorem Rat.echelonAux_isEchelon : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : ((x3 : AxNat) -> ((x4 : AxNat) -> Rat))) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : AxNat.le x5 x1) -> ((x7 : ((x7 : AxNat) -> ((x8 : AxNat.lt (AxNat.succ x7) x4) -> Eq.{1} Bool (Rat.echelonStepOk (Rat.leadingIndex x3 x7 x1) (Rat.leadingIndex x3 (AxNat.succ x7) x1) x1) Bool.true))) -> ((x8 : ((x8 : AxNat) -> ((x9 : AxNat.lt x8 x4) -> AxNat.lt (Rat.leadingIndex x3 x8 x1) x5))) -> ((x9 : ((x9 : AxNat) -> ((x10 : AxNat) -> ((x11 : AxNat.le x4 x9) -> ((x12 : AxNat.lt x9 x0) -> ((x13 : AxNat.lt x10 x5) -> Eq.{1} Rat (x3 x9 x10) Rat.zero)))))) -> ((x10 : AxNat.le x1 (AxNat.add x5 x2)) -> Eq.{1} Bool (Rat.isEchelon (Rat.echelonAux x0 x1 x2 x3 x4 x5) x0 x1) Bool.true)))))))))))

Dependencies

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

26 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

rat-row-echelon-is-echelon-1

Kind: kernel-term
Status: checked

Supports: Both forms are checked, axiom-free theorems in all four rational preludes, populations pinned separately at four. The wrapper's regex is anchored on the COMPOSITE `Rat.isEchelon (Rat.rowEchelon x0 x1 x2) x1 x2` -- the predicate applied to the REDUCED matrix, at the same dimensions the reduction was given -- so a statement about the input matrix, or one that reduced at different dimensions from those it tests at, fails. The loop form's regex likewise pins `Rat.echelonAux x0 x1 x2 x3 x4 x5` inside `Rat.isEchelon … x0 x1`. Both pin the axiom-footprint column at 0, which is the headline for this family: obligation 4 closes with no assumption added.

Checker command

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

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The registered evaluation test in `rat_prelude/echelon_invariant_tests.rs` reduces `Rat.isEchelon` to `true` on the reduced matrix AND to `false` on the INPUT, at `[[0,1],[2,3]]` (whose first column is zero at row 0, so the pivot step must swap) and at `[[0,0,2],[0,3,4],[5,6,7]]` (whose row order is reversed). A `rowEchelon` that returned its argument, or an `isEchelon` that accepted everything, fails that pair -- which is the check that stops this fact from being vacuously true.

rat-row-echelon-is-echelon-2

Kind: kernel-term
Status: checked

Supports: Both forms are checked, axiom-free theorems in all four rational preludes, populations pinned separately at four. The wrapper's regex is anchored on the COMPOSITE `Rat.isEchelon (Rat.rowEchelon x0 x1 x2) x1 x2` -- the predicate applied to the REDUCED matrix, at the same dimensions the reduction was given -- so a statement about the input matrix, or one that reduced at different dimensions from those it tests at, fails. The loop form's regex likewise pins `Rat.echelonAux x0 x1 x2 x3 x4 x5` inside `Rat.isEchelon … x0 x1`. Both pin the axiom-footprint column at 0, which is the headline for this family: obligation 4 closes with no assumption added.

Checker command

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

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The registered evaluation test in `rat_prelude/echelon_invariant_tests.rs` reduces `Rat.isEchelon` to `true` on the reduced matrix AND to `false` on the INPUT, at `[[0,1],[2,3]]` (whose first column is zero at row 0, so the pivot step must swap) and at `[[0,0,2],[0,3,4],[5,6,7]]` (whose row order is reversed). A `rowEchelon` that returned its argument, or an `isEchelon` that accepted everything, fails that pair -- which is the check that stops this fact from being vacuously true.

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