Two zero rows in a row pass the echelon step test

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

Recorded description

For every natural number cols, Rat.echelonStepOk cols cols cols is true. This is the SECOND disjunct of the test at the only pair of values that can satisfy it: a leading index is at most cols, so Nat.ble cols l says l = cols, and ADR-1554 records that this disjunct needs BOTH conjuncts because dropping either would accept a nonzero row sitting below a zero one. Two adjacent zero rows are the one case the strict clause cannot cover, and they are exactly what the row-echelon loop invariant produces below its last pivot.

Formal statement

theorem Rat.echelonStepOk_both_cols : ((x0 : AxNat) -> Eq.{1} Bool (Rat.echelonStepOk x0 x0 x0) Bool.true)

Dependencies

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

3 direct dependencies 1 direct dependents

Evidence

rat-echelon-step-ok-both-cols-1

Kind: kernel-term
Status: checked

Supports: A checked, axiom-free theorem in all four rational preludes, population pinned at four. The regex requires all THREE arguments to be the same variable `x0`: the statement is about the diagonal, and a version quantified over two independent leading indices would be false.

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_both_cols[[:space:]]+0[[:space:]].*Eq\.\{1\} Bool \(Rat\.echelonStepOk x0 x0 x0\) Bool\.true\)$')" = 4

Evidence notes

Run 2026-09-02: four rows, mutation-checked by `scripts/new-fact.py`. This is the disjunct that accepts two adjacent zero rows, which is exactly what the row-echelon loop invariant produces below its last pivot -- every such row is zero across the full width, so F:rat-leading-index-eq-cols-of-zero-row reads `cols` for it.

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