The leading-index scan reads nothing but its own row

Identifier: F:rat-leading-index-congr-row
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every pair of matrices M, N : Nat -> Nat -> Rat, every pair of row indices r, r' and every column count cols, IF (for all j, Eq Rat (M r j) (N r' j)) THEN Eq Nat (Rat.leadingIndex M r cols) (Rat.leadingIndex N r' cols), and likewise for the fuelled form Rat.leadingIndexAux at every fuel and every starting column. In words: the leading-index scan reads nothing but its own row, so two matrices agreeing on one row agree on that row's leading index. THE HYPOTHESIS IS POINTWISE AND STAYS POINTWISE: nothing here equates the two matrices, so no function extensionality is used or needed. ADR-1555 recorded that the ROW form of rank invariance under an elementary operation does need funext because it must equate two matrices; this is the statement that lets the row-echelon loop invariant's clause about the ALREADY-PROCESSED prefix survive a pivot step without it, since F:rat-clear-below-row-swap-off supplies exactly a pointwise agreement on those rows. The proof spends NO Bool split: one transport moves the recursive call along the induction hypothesis and a second moves the tested entry along the row hypothesis, and the surrounding branch structure is literally the same term on both sides, so the obvious two-way case analysis on Nat.ble cols c and Rat.isZeroB is never performed.

Formal statement

theorem Rat.leadingIndex_congr_row : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : ((x1 : AxNat) -> ((x2 : AxNat) -> Rat))) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : ((x5 : AxNat) -> Eq.{1} Rat (x0 x2 x5) (x1 x3 x5))) -> Eq.{1} AxNat (Rat.leadingIndex x0 x2 x4) (Rat.leadingIndex x1 x3 x4))))))) ; theorem Rat.leadingIndexAux_congr_row : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : ((x1 : AxNat) -> ((x2 : AxNat) -> Rat))) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : ((x5 : AxNat) -> Eq.{1} Rat (x0 x2 x5) (x1 x3 x5))) -> ((x6 : AxNat) -> ((x7 : AxNat) -> Eq.{1} AxNat (Rat.leadingIndexAux x0 x2 x4 x6 x7) (Rat.leadingIndexAux x1 x3 x4 x6 x7)))))))))

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

rat-leading-index-congr-row-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 two regexes are anchored on the ROW INDICES: the left scan reads `x2` of `x0` and the right reads `x3` of `x1`, so a statement that had silently used the same row index on both sides -- which is what a copied congruence lemma degenerates to -- fails the check. They also pin the axiom-footprint column at `0`, which matters here because a `funext` route would not be axiom-free in this kernel.

Checker command

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

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The registered evaluation tests are in `rat_prelude/echelon_invariant_tests.rs`: at `M = [[0,0,5],[1,2,3]]` and `N = [[9,9,9],[0,0,5]]`, which agree on `M`'s row 0 and `N`'s row 1, both leading indices reduce to 2 -- and the OTHER row of each reduces to 0, so the two matrices are shown NOT to agree everywhere and the hypothesis is doing work. The theorem is then applied at fully free arguments with a control that refuses the version whose right-hand row index is `r` rather than `r'`.

rat-leading-index-congr-row-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 two regexes are anchored on the ROW INDICES: the left scan reads `x2` of `x0` and the right reads `x3` of `x1`, so a statement that had silently used the same row index on both sides -- which is what a copied congruence lemma degenerates to -- fails the check. They also pin the axiom-footprint column at `0`, which matters here because a `funext` route would not be axiom-free in this kernel.

Checker command

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

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The registered evaluation tests are in `rat_prelude/echelon_invariant_tests.rs`: at `M = [[0,0,5],[1,2,3]]` and `N = [[9,9,9],[0,0,5]]`, which agree on `M`'s row 0 and `N`'s row 1, both leading indices reduce to 2 -- and the OTHER row of each reduces to 0, so the two matrices are shown NOT to agree everywhere and the hypothesis is doing work. The theorem is then applied at fully free arguments with a control that refuses the version whose right-hand row index is `r` rather than `r'`.

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-1571-obligation-3-closes-obligation-2-completes-and-obligation-4-is-four-lemmas-not-one.md"
}