Round-six lemma `leB_sound`
ProvedIntMul.Kappa.R6.Cx.NetF2.leB_soundAn 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.R6CxNetF2):
theorem IntMul.Kappa.R6.Cx.NetF2.leB_sound : ∀ (U V : Code), okC U = true → okC V = true → leB U V = true → IntMul.Kappa.R6.Cx.NetF2.dec U ≤ IntMul.Kappa.R6.Cx.NetF2.dec V
Context. Labels of the h = 24 local program: codes over 𝔽₂^24 and a sound Boolean edge checker
A label code (Code) is one of
coord X:span {e_p : p ∈ X};psp a b C:span {e_a + e_b + e_c : c ∈ C}(a "pair span"; a line⟨t⟩ispsp p q {r});perp t:⟨t⟩^⊥(a triplet);ext k: boundary labels of stage two (decoded elsewhere).
Vectors are 24-bit naturals (bitv). edgeB new old = true implies
NetComplexP8.EdgeOK (dec new) (dec old) (edgeB_sound), with finrank (dec c) = dimC c
(finrank_dec). All functions are kernel-friendly (straight-line bit operations, SWAR popcount).
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_Defs24 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx IntMul.Kappa.R6.Cx.NetF2 open Matrix Finset Matrix.Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8
theorem IntMul.Kappa.R6.Cx.NetF2.leB_sound : ∀ (U V : Code), okC U = true → okC V = true → leB U V = true → IntMul.Kappa.R6.Cx.NetF2.dec U ≤ IntMul.Kappa.R6.Cx.NetF2.dec V := by sorry