One pivot (round six, `elQ`)
ProvedJ6Seg.PJ.Rn.elQOne pivot, on any stacks D with the matrix on 14, the lines on 30, 16, 51 empty.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJD2):
theorem J6Seg.PJ.Rn.elQ {v w : Vr} {D : Cs} (hq : q < m) (hW1 : 1 ≤ W) (hmW : m * m + m ≤ 2 ^ W)
(hw : BV W w) (hF : Fr v w) (h1 : w 1 = q) (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 2 ^ (Q + 1))
(h28 : v 28 = m) (h11 : v 11 = mw) (h12 : v 12 = cB)
(hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m)
(hM : D 14 = matL (Mseq Q (bandS mw cB) L A q) m) (h16 : D 16 = []) (h51 : D 51 = [])
(hB : ∀ q ≤ m, ∀ i < m, ∀ k < m, |Mseq Q (bandS mw cB) L A q i k| ≤ 2 ^ B) (hBW : B ≤ W)
(hLb : ∀ j ∈ L, j ≤ 2 ^ W) :
Rn J6Seg.PJ.elQ w D (fun w' => Fr v w' ∧ w' 1 = q ∧ BV W w')
(update D 14 (matL (Mseq Q (bandS mw cB) L A (q + 1)) m)) (cQ W m)
Context. B-line IL, J pre-table (B5-J), jTab part D2: the pattern elimination stage (program)
elQ: one pivot q (on 1): 3 := m²; for x < m² push Mseq (q+1) at x onto 16
(elB); pop the old matrix off 14; move 16 back onto 14 (row-major again).
elimP = forL 50 28 1 elQ, and Rn.elimP: from c 14 = matL (Mseq 0) m to
matL (Mseq m) m, registers outside 1–8, 29 unchanged, at cost cElim W m.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs71
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function J6Seg.PJ.E
variable {Q W B m mw cB q : ℕ} {L : List ℕ} {A : ℕ → ℕ → ℤ}
theorem J6Seg.PJ.Rn.elQ {v w : Vr} {D : Cs} (hq : q < m) (hW1 : 1 ≤ W) (hmW : m * m + m ≤ 2 ^ W)
(hw : BV W w) (hF : Fr v w) (h1 : w 1 = q) (h9 : v 9 = 2 ^ Q) (h10 : v 10 = 2 ^ (Q + 1))
(h28 : v 28 = m) (h11 : v 11 = mw) (h12 : v 12 = cB)
(hL : D 30 = L.map (fun j : ℕ => (j : ℤ))) (hLm : L.length = m)
(hM : D 14 = matL (Mseq Q (bandS mw cB) L A q) m) (h16 : D 16 = []) (h51 : D 51 = [])
(hB : ∀ q ≤ m, ∀ i < m, ∀ k < m, |Mseq Q (bandS mw cB) L A q i k| ≤ 2 ^ B) (hBW : B ≤ W)
(hLb : ∀ j ∈ L, j ≤ 2 ^ W) :
Rn J6Seg.PJ.elQ w D (fun w' => Fr v w' ∧ w' 1 = q ∧ BV W w')
(update D 14 (matL (Mseq Q (bandS mw cB) L A (q + 1)) m)) (cQ W m) := by sorry