Row-echelon form implies the pivot section

Identifier: F:rat-pivot-section-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 r with Nat.Lt r rows and Rat.nonzeroRowB E cols r true, Rat.pivotRowOfCol E rows cols (Rat.pivotColOfRow E cols r) equals r. This is the implication ADR-1562 section 2 identified as the residue of ADR-1554's obligation 4 -- 'the first row whose leading index is row r's is r itself' -- and which ADR-1574 made derivable by closing that obligation. Rat.nonzeroRowB E cols r = true IS Nat.ble (succ (Rat.leadingIndex E r cols)) cols = true, i.e. the row leads strictly inside the width, which is exactly the hypothesis the chain lemma needs to run down from r; every row above r then leads strictly left of it, so none can match, and the scan characterisation answers r. THE HYPOTHESIS IS A REAL CONSTRAINT: ADR-1562 exhibits [[1,0],[1,0]], two nonzero rows sharing leading index 0, where the section equation is FALSE at row 1 -- and Rat.isEchelon says false there, which is checked by reduction.

Formal statement

theorem Rat.pivotSection_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 x4 x1) -> ((x6 : Eq.{1} Bool (Rat.nonzeroRowB x0 x2 x4) Bool.true) -> Eq.{1} AxNat (Rat.pivotRowOfCol x0 x1 x2 (Rat.pivotColOfRow x0 x2 x4)) x4)))))))

Dependencies

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

4 direct dependencies 3 direct dependents

Evidence

rat-pivot-section-of-is-echelon-1

Kind: kernel-term
Status: checked

Supports: A checked, axiom-free theorem in all four rational preludes, population pinned at four. The regex is anchored on the COMPOSITE round trip `Rat.pivotRowOfCol x0 x1 x2 (Rat.pivotColOfRow x0 x2 x4)` equalling `x4` -- the two maps in that order, with the row index recovered -- so the trivial equation between a leading index and a row index fails. It also pins 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\.pivotSection_of_isEchelon[[:space:]]+0[[:space:]].*Eq\.\{1\} AxNat \(Rat\.pivotRowOfCol x0 x1 x2 \(Rat\.pivotColOfRow x0 x2 x4\)\) x4\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows, mutation-checked by `scripts/new-fact.py`. The registered evidence that the ANTECEDENT is not met by every matrix is in `rat_prelude/echelon_section_tests.rs`: ADR-1562 section 2 exhibits `[[1,0],[1,0]]` as the shape where the section equation is FALSE at row 1, and `Rat.isEchelon` reduces to `false` there while the same matrix REDUCED reduces to `true`. Without that pair the implication could be vacuous or could be deriving a false conclusion from a satisfied hypothesis.

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