Round-six lemma `kmulD_bnd`
ProvedJ6Seg.KR.kmulD_bndAn 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.J6SegKr4):
theorem J6Seg.KR.kmulD_bnd {b r p Δ : ℕ} (hb : 1 ≤ b) (hbig : 2 * r * 2 ^ (2 * p) < 2 ^ (b - 1))
{zx zy : List GI} (hzx : ∀ z ∈ zx, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p)
(hzy : ∀ z ∈ zy, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p) : GB (b + 2) (kmulD r Δ zx zy)
Context. B3 (chunk kernel), part 4: the Toeplitz stage
tsI pM IN OUTS: with n on bN, 2n on bN2, a Gaussian block t (reversed, gflat t.reverse)
on IN, the real table am (length n) on top of the table stack dT, and the record-product
parameters for records of length r = 2n on the parameter stacks 50 … 55 (managed), it leaves
gflat (lwG P (2n) am t) on OUTS, consumes am from dT onto the stack DU of consumed
descriptors, and uses one uniform Kronecker record product (recU, Δ = 0).
The parameter stacks are managed lists here; around recU they are moved into the base state
(encK_split).
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_Defs62
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFV
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
theorem J6Seg.KR.kmulD_bnd {b r p Δ : ℕ} (hb : 1 ≤ b) (hbig : 2 * r * 2 ^ (2 * p) < 2 ^ (b - 1))
{zx zy : List GI} (hzx : ∀ z ∈ zx, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p)
(hzy : ∀ z ∈ zy, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p) : GB (b + 2) (kmulD r Δ zx zy) := by sorry