A leading entry that moved strictly right passes the echelon step test

Identifier: F:rat-echelon-step-ok-of-lt
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For all natural numbers l1, l2 and cols, IF Nat.Lt l1 l2 THEN Rat.echelonStepOk l1 l2 cols is true. This is the FIRST disjunct of the test as a lemma, and it holds whatever cols is -- the strict clause does not mention it. It is what fires at the boundary of the row-echelon loop invariant, where the last placed row leads strictly left of the cursor and the row below it is the freshly placed pivot.

Formal statement

theorem Rat.echelonStepOk_of_lt : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat.lt x0 x1) -> Eq.{1} Bool (Rat.echelonStepOk x0 x1 x2) Bool.true))))

Dependencies

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

2 direct dependencies 3 direct dependents

Evidence

rat-echelon-step-ok-of-lt-1

Kind: kernel-term
Status: checked

Supports: A checked, axiom-free theorem in all four rational preludes, population pinned at four. The regex pins the conclusion at `Bool.true` and the argument order `x0 x1 x2` -- the test is NOT symmetric in its first two arguments, and swapping them turns a true statement into a false one.

Checker command

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

Evidence notes

Run 2026-09-02: four rows, mutation-checked by `scripts/new-fact.py`. Spent at the boundary of the row-echelon loop invariant, where the last placed row leads strictly left of the column cursor and the row below it is the freshly placed pivot, whose leading index is the cursor exactly.

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