The echelon predicate can be read back as the adjacent-pair condition

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

Recorded description

For every matrix E : Nat -> Nat -> Rat and every rows, cols, IF Rat.isEchelon E rows cols is true THEN for every q with Nat.Lt (Nat.succ q) rows the test Rat.echelonStepOk (Rat.leadingIndex E q cols) (Rat.leadingIndex E (Nat.succ q) cols) cols is true -- and likewise for the fuelled form Rat.isEchelonAux from any starting row, given the pair is one the call will visit. This is the converse of F:rat-is-echelon-of-pairs. THE FUEL BOUND IS FORCED HERE AND ABSENT THERE, and that asymmetry is ADR-1571 section 2's rule seen from both sides: isEchelonAux answers true when its fuel runs out, which SATISFIES the forward conclusion and FALSIFIES this one, because this direction concludes something about a pair an exhausted scan may never have reached. Nat.Lt q (Nat.add r fuel) -- the pair is one of the fuel rows this call will visit -- is the weakest thing that rules that out.

Formal statement

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

Dependencies

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

9 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

rat-pairs-of-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. Each regex is anchored on the CONCLUSION being the step test at the pair `(q, succ q)` and equal to `Bool.true`, so a statement about a different pair, or one concluding `Bool.false`, 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\.pairs_of_isEchelonAux[[:space:]]+0[[:space:]].*Eq\.\{1\} Bool \(Rat\.echelonStepOk \(Rat\.leadingIndex x0 x3 x2\) \(Rat\.leadingIndex x0 \(AxNat\.succ x3\) x2\) x2\) Bool\.true\)\)\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The pair with F:rat-is-echelon-of-pairs is the evidence that the fuel bound is not decoration: the two facts are the two directions of the same equivalence and only ONE of them carries a bound, which is ADR-1571 section 2's rule made visible in the ledger rather than only in prose.

rat-pairs-of-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. Each regex is anchored on the CONCLUSION being the step test at the pair `(q, succ q)` and equal to `Bool.true`, so a statement about a different pair, or one concluding `Bool.false`, 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\.pairs_of_isEchelon[[:space:]]+0[[:space:]].*Eq\.\{1\} Bool \(Rat\.echelonStepOk \(Rat\.leadingIndex x0 x4 x2\) \(Rat\.leadingIndex x0 \(AxNat\.succ x4\) x2\) x2\) Bool\.true\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The pair with F:rat-is-echelon-of-pairs is the evidence that the fuel bound is not decoration: the two facts are the two directions of the same equivalence and only ONE of them carries a bound, which is ADR-1571 section 2's rule made visible in the ledger rather than only in prose.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/echelon_section.rs)",
  "source": "docs/research/09-decisions/adr-1574-obligation-4-closes-and-the-exit-derivation-folds-into-the-induction.md"
}