The row-echelon Bool predicate is exactly the adjacent-pair condition

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

Recorded description

For every matrix M : Nat -> Nat -> Rat and every rows, cols, IF for all q with Nat.Lt (Nat.succ q) rows the test Rat.echelonStepOk (Rat.leadingIndex M q cols) (Rat.leadingIndex M (Nat.succ q) cols) cols is true, THEN Rat.isEchelon M rows cols is true -- and likewise for the fuelled form Rat.isEchelonAux from any starting row, with the pair condition restricted to rows at or below that start. In words: the computed Bool predicate is discharged by checking each adjacent pair, which is what turns a loop invariant about leading indices into the predicate itself. THERE IS NO FUEL BOUND, and ADR-1571 section 2's rule forces that: isEchelonAux answers true when its fuel runs out and true is the conclusion, so the exhaustion answer satisfies the postcondition directly -- the exact opposite of F:rat-pivot-search-ge-start, whose exhaustion answer falsifies its conclusion and which therefore has to refute both exhaustion leaves.

Formal statement

theorem Rat.isEchelon_of_pairs : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : ((x3 : AxNat) -> ((x4 : AxNat.lt (AxNat.succ x3) x1) -> Eq.{1} Bool (Rat.echelonStepOk (Rat.leadingIndex x0 x3 x2) (Rat.leadingIndex x0 (AxNat.succ x3) x2) x2) Bool.true))) -> Eq.{1} Bool (Rat.isEchelon x0 x1 x2) Bool.true)))) ; theorem Rat.isEchelonAux_of_pairs : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : ((x5 : AxNat) -> ((x6 : AxNat.le x4 x5) -> ((x7 : AxNat.lt (AxNat.succ x5) x1) -> Eq.{1} Bool (Rat.echelonStepOk (Rat.leadingIndex x0 x5 x2) (Rat.leadingIndex x0 (AxNat.succ x5) x2) x2) Bool.true)))) -> Eq.{1} Bool (Rat.isEchelonAux x0 x1 x2 x3 x4) Bool.true))))))

Dependencies

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

4 direct dependencies 2 direct dependents

Evidence

rat-is-echelon-of-pairs-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 regexes are anchored on the CONCLUSION being `= Bool.true`, not merely on the predicate appearing: a statement that concluded `= Bool.false`, or that concluded about `Rat.echelonStepOk` rather than `Rat.isEchelon`, fails. They also pin 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\.isEchelonAux_of_pairs[[:space:]]+0[[:space:]].*Eq\.\{1\} Bool \(Rat\.isEchelonAux x0 x1 x2 x3 x4\) Bool\.true\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The registered evidence that the predicate is not vacuous is in `rat_prelude/echelon_invariant_tests.rs`, where `Rat.isEchelon` reduces to `false` on `[[0,1],[2,3]]` and on `[[0,0,2],[0,3,4],[5,6,7]]` -- so an `isEchelon` that accepted everything would fail there and this fact would be worthless.

rat-is-echelon-of-pairs-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 regexes are anchored on the CONCLUSION being `= Bool.true`, not merely on the predicate appearing: a statement that concluded `= Bool.false`, or that concluded about `Rat.echelonStepOk` rather than `Rat.isEchelon`, fails. They also pin 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\.isEchelon_of_pairs[[:space:]]+0[[:space:]].*Eq\.\{1\} Bool \(Rat\.isEchelon x0 x1 x2\) Bool\.true\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The registered evidence that the predicate is not vacuous is in `rat_prelude/echelon_invariant_tests.rs`, where `Rat.isEchelon` reduces to `false` on `[[0,1],[2,3]]` and on `[[0,0,2],[0,3,4],[5,6,7]]` -- so an `isEchelon` that accepted everything would fail there and this fact would be worthless.

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