Round-six lemma `DC_vals`
ProvedIntMul.Kappa.R6.Bit.NB.DC_valsAn 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 R6Pk.R6BitNBNetE):
theorem IntMul.Kappa.R6.Bit.NB.DC_vals : (List.range 23).map DC = [2668, 45080, 26286, 8326, 12804, 9110, 3607, 3026, 3285, 2451,
3515, 1255, 3239, 1600, 3308, 1968, 4159, 1255, 10043, 3926, 1288, 2750, 3565]
Context. Round six, bit network: the child-width histogram and BitNetR6MomStmt
Every edge of the network contributes the moment of its runs: side edges of rank r give
f (2r - 23) + (23 - r) f 1 (2r > 23) or r f 1, aux edges f 23 + f 483, data edges
f 439 + f 21 + 24 f 1. The per-rank move counts of the two stage words are the base-2³² digits
of the kernel-checked packed counts CNs1, CNs2 (no overflow: touch1, touch2). The total
moment equals Jain's bitR6 moment.
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_Defs52 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit IntMul.Kappa.R6.Bit.NB open Matrix R6Chk R6Chk.Bit R6Chk.Bit.Loc AModel AModelFac
theorem IntMul.Kappa.R6.Bit.NB.DC_vals : (List.range 23).map DC = [2668, 45080, 26286, 8326, 12804, 9110, 3607, 3026, 3285, 2451,
3515, 1255, 3239, 1600, 3308, 1968, 4159, 1255, 10043, 3926, 1288, 2750, 3565] := by sorry