Round-six lemma `bitNetR6_mom`
ProvedIntMul.Kappa.R6.Bit.NB.bitNetR6_momAn 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.bitNetR6_mom : BitNetR6MomStmt
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.bitNetR6_mom : BitNetR6MomStmt := by sorry