Round-six lemma `sHr`
ProvedIntMul.Kappa.R6.IL2.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.R6IL2Head):
theorem IntMul.Kappa.R6.IL2.sHr : ESp eHr u Bb ((hR i j : ℕ) : ℤ)
Context. Round six, item language (I2): the row-addition header for any label dimension m
Parametric copy of the m-dependent part of KFX5Head (the frozen file has the OpenAI label
dimension mC = 100^3 hard-wired): the register assignment rowσ m … of the ten row-addition
parameters [m^k, K, e, t, S0, B, r, H, i, j] (i j : Fin m), the shape factors N0R … N3R,
the admissibility facts PF m … (now also 6 ≤ K and 16 ≤ m ≤ 10^6; round six has m = 576),
and the specifications x… of the header expressions (the expressions themselves are the frozen
ones: they read m^k from a register, so they do not depend on 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_Defs13
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH NLogN.KFX AModel Butterfly
variable {m k K e T S0 B r H : ℕ} {i j : Fin m} {u : IState HS} {Bb : ℕ}
(hp : PF m k K e T S0 B r) (hA : Agree (rowσ m 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 IntMul.Kappa.R6.IL2.sHr : ESp eHr u Bb ((hR i j : ℕ) : ℤ) := by sorry