`recU_runs` with a general truncation `Δ` (round six, `recU_runsD`)
ProvedJ6Seg.recU_runsDrecU_runs with a general truncation Δ: vO receives the reversed kmulD r Δ zx zy.
The following holds (Lean statement, in the scope of module Solutions.J6SegKr0):
theorem J6Seg.recU_runsD {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
{b r p Δ φ : ℕ} (hΦ : ∀ x y : ℤ, zsz x ≤ b * r + 2 → zsz y ≤ b * r + 2 → M.Φ x y ≤ φ)
(hb : 1 ≤ b) (hr : 1 ≤ r) (hbig : 2 * r * 2 ^ (2 * p) < 2 ^ (b - 1))
(s : IState HS) (f : Fin HS → List ℤ) (zx zy : List GI) (lx ly : List ℤ)
(hX : f vX = gflat zx ++ lx) (hY : f vY = gflat zy ++ ly) (hlx : zx.length = r)
(hly : zy.length = r)
(hzx : ∀ z ∈ zx, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p) (hzy : ∀ z ∈ zy, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p)
(hT : Tmp f)
(hP : PV (πr (2 ^ p) (NLogN.KFV.kG b r (2 ^ p)) b r ((2 ^ b) ^ (2 * r)) (2 ^ Δ)) s)
(hF : PZ (πr (2 ^ p) (NLogN.KFV.kG b r (2 ^ p)) b r ((2 ^ b) ^ (2 * r)) (2 ^ Δ)) f) :
IRuns I iprog (recU pM) (encK s f)
(encK s (Function.update (Function.update (Function.update f vX lx) vY ly) vO
((gflat (kmulD r Δ zx zy)).reverse ++ f vO)))
(2000 * cRec r p b Δ φ)
Context. B3 (chunk kernel), part 0: one uniform Kronecker record product with general truncation
KFV10Rec.recU_runs with the truncation Δ free (there Δ = p + ρ; the program recU reads
2^Δ from the parameter stack kD): on records zx, zy of length r (entries |·| ≤ 2^p,
digit width b with 2 r 2^{2p} < 2^{b-1}), recU leaves the reversed record
kmulD r Δ zx zy, entry j = the y^r + 1-folded numerators truncated by 2^Δ.
With Δ = 0 and zero-padded records this is the exact Gaussian polynomial product
(the Toeplitz stages of the chunk kernel).
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 NLogN NLogN.KFV
set_option maxRecDepth 10000
open IntMul NLogN.KIL NLogN.KFD NLogN.KFT NLogN.KFB NLogN.KFC NLogN.RS
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
open J6Seg Synth
theorem J6Seg.recU_runsD {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
{b r p Δ φ : ℕ} (hΦ : ∀ x y : ℤ, zsz x ≤ b * r + 2 → zsz y ≤ b * r + 2 → M.Φ x y ≤ φ)
(hb : 1 ≤ b) (hr : 1 ≤ r) (hbig : 2 * r * 2 ^ (2 * p) < 2 ^ (b - 1))
(s : IState HS) (f : Fin HS → List ℤ) (zx zy : List GI) (lx ly : List ℤ)
(hX : f vX = gflat zx ++ lx) (hY : f vY = gflat zy ++ ly) (hlx : zx.length = r)
(hly : zy.length = r)
(hzx : ∀ z ∈ zx, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p) (hzy : ∀ z ∈ zy, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p)
(hT : Tmp f)
(hP : PV (πr (2 ^ p) (NLogN.KFV.kG b r (2 ^ p)) b r ((2 ^ b) ^ (2 * r)) (2 ^ Δ)) s)
(hF : PZ (πr (2 ^ p) (NLogN.KFV.kG b r (2 ^ p)) b r ((2 ^ b) ^ (2 * r)) (2 ^ Δ)) f) :
IRuns I iprog (recU pM) (encK s f)
(encK s (Function.update (Function.update (Function.update f vX lx) vY ly) vO
((gflat (kmulD r Δ zx zy)).reverse ++ f vO)))
(2000 * cRec r p b Δ φ) := by sorry