Round-six lemma `exNet_OK`
ProvedIntMul.Kappa.R6.Bit.exNet_OKAn 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.R6BitEx):
theorem IntMul.Kappa.R6.Bit.exNet_OK (N : ℕ) [NeZero N] : (exNet (R := R)).OK N
Context. Round six, bit side: a sanity instance of QHNet.OK
exNet: m = 2, one role, no temporaries, a single edge with trivial Bruhat factors and the
two runs H₀ ↔ D₀, H₁ ↔ D₁ (widths 1 < m). It satisfies QHNet.OK N at every field size
(exNet_OK), via idealOK_of_labels. This checks that the hypotheses of prop11H are
consistent (non-vacuous); of course this network has no saving (histMoment = 2 (1/2)^τ ≥ 1).
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_Defs4
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit
open AModel AModelFac Matrix
variable {R : Type*} [CommRing R]
theorem IntMul.Kappa.R6.Bit.exNet_OK (N : ℕ) [NeZero N] : (exNet (R := R)).OK N := by sorry