Round-six lemma `sHr`
ProvedNLogN.KFX.sHrAn 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.KFX5Head):
theorem NLogN.KFX.sHr : ESp eHr u Bb ((hR i j : ℕ) : ℤ)
Context. KFX §5: the header of the uniform row addition
From the row-addition parameters on the background stacks 36 … 45
([mC^k, K, e, t, S0, B, r, H, i, j]) the header computes the master registers σMR of
l13U: the third row h ∉ {i, j}, the sorted rows s0 < s1 < s2, the slots px, py, the
factors N0 … N3 of the shape shR, Q = 2^{fK}, 2^K, 2^ρ (ρ = e % K), the swap flags,
gx, and (by a halving loop) A = zsz V.
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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFX
open IntMul NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH AModel Butterfly
variable {k K e T S0 B r H : ℕ} {i j : Fin mC} {u : IState HS} {Bb : ℕ}
(hp : PF k K e T S0 B r) (hA : Agree (rowσ k K e T S0 B r H i j) u)
(hBb : zsz ((VbR T S0 B r H : ℕ) : ℤ) ≤ Bb)
include hp hA hBb
theorem NLogN.KFX.sHr : ESp eHr u Bb ((hR i j : ℕ) : ℤ) := by sorry