Round-six lemma `C832L_eq`
ProvedR6Chk.C832L_eqAn 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 Solutions.R6ChkConst):
theorem R6Chk.C832L_eq : C832L = C832
Context. Literal constants for the packed kernels
The constants of R6ChkPack as numeric literals (so that kernel reduction never recomputes them),
each proved equal to its definition by one kernel evaluation.
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_K_Defs33 import Definitions.Def_IntMul_Kappa_R6_Defs1 import Mathlib import Definitions.Def_IntMul_Kappa_R6_Defs9 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open R6Chk
theorem R6Chk.C832L_eq : C832L = C832 := by sorry