A pivot column recovers its own index from the row the search found

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

Recorded description

For every matrix E : Nat -> Nat -> Rat, all dimensions rows, cols and every column j, IF Rat.isPivotColB E rows cols j = true THEN Rat.leadingIndex E (Rat.pivotRowOfCol E rows cols j) cols = j -- the row the search returned for a pivot column really does lead in that column. The underlying statement about the fuelled scan is the same with the hypothesis replaced by its content: if Rat.pivotRowSearchAux E rows cols j fuel r lands strictly below rows, its leading index is j. The in-range hypothesis carries the whole proof: both exhaustion answers are rows itself, which Nat.lt_irrefl refutes, so the two gave-up branches are discharged without knowing anything about the matrix. This is the round trip that makes the bridge's orientation the cheap one -- it supplies THREE of Nat.countRange_bij's five hypotheses at once when the columns are taken as the left-hand count: injectivity of Rat.pivotRowOfCol (apply the leading index to both sides), the selected half of its MapsInto (the leading index of the row found is the column asked for, which is below cols), and one round-trip equation verbatim.

Formal statement

theorem Rat.leadingIndex_pivotRowOfCol : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : Eq.{1} Bool (Rat.isPivotColB x0 x1 x2 x3) Bool.true) -> Eq.{1} AxNat (Rat.leadingIndex x0 (Rat.pivotRowOfCol x0 x1 x2 x3) x2) x3))))) ; theorem Rat.pivotRowSearchAux_leadingIndex : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : AxNat.lt (Rat.pivotRowSearchAux x0 x1 x2 x3 x4 x5) x1) -> Eq.{1} AxNat (Rat.leadingIndex x0 (Rat.pivotRowSearchAux x0 x1 x2 x3 x4 x5) x2) x3)))))))

Dependencies

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

2 direct dependencies 1 direct dependents

Evidence

rat-leading-index-pivot-row-of-col-1

Kind: kernel-term
Status: checked

Supports: Both `Rat.leadingIndex_pivotRowOfCol` and the fuelled `Rat.pivotRowSearchAux_leadingIndex` are checked `Declaration::Theorem`s with EMPTY axiom footprints in all four preludes. The checker counts EIGHT rows -- two declarations across four preludes -- and requires exactly that, so losing either half changes the count and the command exits 1. The regex pins the CONCLUSION to `Rat.leadingIndex x0 (Rat.pivotRow… …) x2 = x3`, i.e. the leading index taken at the COLUMN COUNT `x2` and equal to the COLUMN ASKED FOR `x3`: a version concluding the leading index equals the row index, or taken at the row count, would not match.

Checker command

out=$(target/release/examples/kernel_declaration_projection 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^(rat|creal|complex|cpoint)[[:space:]]+theorem[[:space:]]+Rat\.(leadingIndex_pivotRowOfCol|pivotRowSearchAux_leadingIndex)[[:space:]]+0[[:space:]].*Eq\.\{1\} AxNat \(Rat\.leadingIndex x0 \(Rat\.(pivotRowOfCol|pivotRowSearchAux) x0 x1 x2 x3( x4 x5)?\) x2\) x3\)+$')" = 8

Evidence notes

Run 2026-09-02: the pattern matches the real output at exactly the required count. `scripts/new-fact.py` verified it FAILS on mutated output (digits perturbed, true -> false, 0 -> 1) before this file was written, so a pattern anchored on the surrounding prose rather than on the finding would have been rejected there.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/rank_bridge.rs)",
  "source": "docs/research/09-decisions/adr-1562-the-bridge-orientation-is-the-finding-and-obligation-4-collapses-to-one-section-equation.md"
}