The block constants by doubling (round six, `sp_kg`)

The block constants by doubling.

The following holds (Lean statement, in the scope of module Solutions.J6SegKs1):

theorem J6Seg.KR.sp_kg (s : IState HS) (F : Fin HS → List ℤ) {pk b j n Bk : ℕ}
    (hX : F vX = []) (hY : F vY = []) (hCN : F CN = []) (hc : F kc = [2 ^ pk])
    (hB : F kB = [2 ^ b]) (hK : F kK = [(j : ℤ)]) (hJ : F kJ = [((b * (2 * n) : ℕ) : ℤ)])
    (hpk : pk < b) (hnj : 2 * n ≤ 2 ^ j) (hBk : b * 2 ^ j + 2 ≤ Bk)
    (hBm : 2 * (b * (2 * n)) + 2 ≤ Bk) (hBj : zsz (j : ℤ) ≤ Bk) :
    Sp kgRS (encK s F) (encK s (Function.update (Function.update F kK [KFV.kG b (2 * n) (2 ^ pk)])
      kJ [(2 ^ b) ^ (2 * (2 * n))])) (cKG j (b * (2 * n)) Bk)

Context. B3′, part 1: computing the Kronecker constants of a block in the kernel

kgRS (with j on kK, m = b·2n on kJ, 2^pk on kc, 2^b on kB, scratch vX, vY, CN): acc := 2^pk, ρ := 2^b; j times acc := acc + acc·ρ, ρ := ρ·ρ (so acc = KFV.kG b 2^k 2^pk, ρ = 2^(b 2^k)); then kJ := 2^m, kK := acc mod 2^m = KFV.kG b (2n) 2^pk, kJ := 2^m · 2^m. Cost O(j · b 2^j + pow2Cost m) — linear in n b up to the factor j = clog₂ 2n.

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*).