The pivot-row scan answers the first row with the given leading index

Identifier: F:rat-pivot-row-of-col-eq-of-first
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every matrix E : Nat -> Nat -> Rat, every rows, cols, column index j and row r, IF Nat.Lt r rows AND no q below r has Rat.leadingIndex E q cols equal to j AND Rat.leadingIndex E r cols equals j, THEN Rat.pivotRowOfCol E rows cols j equals r -- and likewise for the fuelled form Rat.pivotRowSearchAux from any start, given the exclusion runs from that start and the fuel reaches r. This is the same shape as F:rat-leading-index-eq-of-first-nonzero: nothing before it matches, it matches, and the fuel reaches it. THE FUEL BOUND IS FORCED, because the scan's exhaustion answer is rows and r is in range, so an exhausted scan falsifies the conclusion. It is what turns a uniqueness statement about leading indices into a statement about the COMPUTED scan, which is what ADR-1562's pivot-section equation is phrased in terms of.

Formal statement

theorem Rat.pivotRowOfCol_eq_of_first : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat.lt x4 x1) -> ((x6 : ((x6 : AxNat) -> ((x7 : AxNat.lt x6 x4) -> Not (Eq.{1} AxNat (Rat.leadingIndex x0 x6 x2) x3)))) -> ((x7 : Eq.{1} AxNat (Rat.leadingIndex x0 x4 x2) x3) -> Eq.{1} AxNat (Rat.pivotRowOfCol x0 x1 x2 x3) x4)))))))) ; theorem Rat.pivotRowSearchAux_eq_of_first : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : AxNat) -> ((x7 : AxNat.le x6 x4) -> ((x8 : AxNat.lt x4 x1) -> ((x9 : AxNat.lt x4 (AxNat.add x6 x5)) -> ((x10 : ((x10 : AxNat) -> ((x11 : AxNat.le x6 x10) -> ((x12 : AxNat.lt x10 x4) -> Not (Eq.{1} AxNat (Rat.leadingIndex x0 x10 x2) x3))))) -> ((x11 : Eq.{1} AxNat (Rat.leadingIndex x0 x4 x2) x3) -> Eq.{1} AxNat (Rat.pivotRowSearchAux x0 x1 x2 x3 x5 x6) x4))))))))))))

Dependencies

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

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

Evidence

rat-pivot-row-of-col-eq-of-first-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 pins the ANSWER `x4` -- the row the caller named -- against the scan term, so a statement concluding about `rows` (the scan's exhaustion answer) 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\.pivotRowSearchAux_eq_of_first[[:space:]]+0[[:space:]].*Eq\.\{1\} AxNat \(Rat\.pivotRowSearchAux x0 x1 x2 x3 x5 x6\) x4\)\)\)\)\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The fuel bound is forced and the failure it rules out is concrete: an exhausted scan answers `rows`, and the hypothesis `Nat.Lt r rows` says the answer must not be that. This is the same shape as F:rat-leading-index-eq-of-first-nonzero, deliberately -- the two searches in this family are characterised the same way.

rat-pivot-row-of-col-eq-of-first-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 pins the ANSWER `x4` -- the row the caller named -- against the scan term, so a statement concluding about `rows` (the scan's exhaustion answer) 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\.pivotRowOfCol_eq_of_first[[:space:]]+0[[:space:]].*Eq\.\{1\} AxNat \(Rat\.pivotRowOfCol x0 x1 x2 x3\) x4\)\)\)\)\)\)\)\)$')" = 4

Evidence notes

Run 2026-09-02: four rows each, mutation-checked by `scripts/new-fact.py`. The fuel bound is forced and the failure it rules out is concrete: an exhausted scan answers `rows`, and the hypothesis `Nat.Lt r rows` says the answer must not be that. This is the same shape as F:rat-leading-index-eq-of-first-nonzero, deliberately -- the two searches in this family are characterised the same way.

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