Clearing the block registers (round six, `popF2`)

Clearing the block registers (block constants at the per-block bound).

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

theorem J6Seg.KR.popF2 (s : IState HS) (G : Fin HS → List ℤ) {r0 o dt du : List ℤ}
    {n pk b BH Bk c : ℕ} (hb1 : zsz (n : ℤ) ≤ BH) (hb2 : zsz ((2 * n : ℕ) : ℤ) ≤ BH)
    (hb3 : zsz (NLogN.KFV.kG b (2 * n) (2 ^ pk)) ≤ Bk) (hb4 : zsz ((2 ^ b : ℤ) ^ (2 * (2 * n))) ≤ Bk)
    (hBc : zsz ((c + 1 : ℕ) : ℤ) ≤ BH) :
    Sp popRS
      (encK s (BF G r0 [] [] o dt du [(n : ℤ)] [((2 * n : ℕ) : ℤ)]
        [((2 * n : ℕ) : ℤ)] [NLogN.KFV.kG b (2 * n) (2 ^ pk)] [(2 ^ b) ^ (2 * (2 * n))] [((c + 1 : ℕ) : ℤ)]))
      (encK s (BF G r0 [] [] o dt du [] [] [] [] [] [(c : ℤ)]))
      (14000 * (BH + 2) + 2 * (2 * Bk + 2))

Context. B3′, part 2: the new block header and block clearing

• hdrRS2 = hdrRS; kgRS: reads [n, 2n, j, 2nb] and computes kG b (2n) 2^pk, (2^b)^(4n);
• hdrF2, popF2: the header and the clearing on the block frame BF, with the small header values at BH and the two block constants at the per-block bound BkN b n = 8 n b + 4.

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