Round-six lemma `isPiv_rank1_lower`

Proved

IntMul.Kappa.R6.Bit.NB.isPiv_rank1_lower

by xuanji · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

The following holds (Lean statement, in the scope of module Solutions.R6BitNBRk):

theorem IntMul.Kappa.R6.Bit.NB.isPiv_rank1_lower {a b : ℕ} (B : Matrix (Fin a) (Fin b) K) (u : Fin a → K) (v : Fin b → K)
    (hB : ∀ (i : Fin a) (j : Fin b), i.val < j.val → B i j = u i * v j)
    (h0 : 0 < a) (hb : 0 < b) (hu : u ⟨0, h0⟩ ≠ 0) (hv : v ⟨b - 1, by omega⟩ ≠ 0)
    (l : ℕ) (hl1 : 1 ≤ l) (hla : l < a) (hlb : l + 1 < b)
    (hT : B ⟨l, hla⟩ ⟨l, by omega⟩ ≠ u ⟨l, hla⟩ * v ⟨l, by omega⟩) : IsPiv B l l

Context. Round six, bit network: pivot lemmas

isPiv_block: pivots of a block in the top-right part pass to the whole matrix.
isPiv_diag_of_lower: a lower triangular matrix with nonzero diagonal pivots on its diagonal.
isPiv_mid: an idempotent of rank m - k with invertible k × k corner pivots on the middle diagonal (CornerLib.solution).
isPiv_rank1_lower: a matrix that is rank one strictly above the diagonal pivots at (l, l).
rk_mul_lower, isPiv_side: lower triangular factors keep the rank profile; the pivots of B M A (B with lower triangular top, A with lower triangular right end) are those of M, moved to the top-right corner.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit IntMul.Kappa.R6.Bit.NB
open Matrix Finset
variable {K : Type*} [Field K]

Formal statement

theorem IntMul.Kappa.R6.Bit.NB.isPiv_rank1_lower {a b : ℕ} (B : Matrix (Fin a) (Fin b) K) (u : Fin a → K) (v : Fin b → K)
    (hB : ∀ (i : Fin a) (j : Fin b), i.val < j.val → B i j = u i * v j)
    (h0 : 0 < a) (hb : 0 < b) (hu : u ⟨0, h0⟩ ≠ 0) (hv : v ⟨b - 1, by omega⟩ ≠ 0)
    (l : ℕ) (hl1 : 1 ≤ l) (hla : l < a) (hlb : l + 1 < b)
    (hT : B ⟨l, hla⟩ ⟨l, by omega⟩ ≠ u ⟨l, hla⟩ * v ⟨l, by omega⟩) : IsPiv B l l := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `IntMul.Kappa.R6.Bit.NB.isPiv_rank1_lower`, Solutions/R6BitNBRk.lean (lines 167–226) of the round-six development.

View graph