Correctness of the general procedure (round six, `gen_correct`)
ProvedIntMul.Kappa.R6.IL.gen_correctCorrectness of the general procedure.
The following holds (Lean statement, in the scope of module Solutions.R6ILGen):
theorem IntMul.Kappa.R6.IL.gen_correct (C : Bit.QHNet (ZMod 2) W T m) (q : ℕ) (ad : IStmt HS 1) (hm : 2 ≤ m)
(hq : q.Prime) (hqB : qBound C < q) (hOK : ∀ f, C.EdgesOK (q ^ f)) (hruns : C.RunsOK)
(M Bb : ℕ) (hM : zsz (M : ℤ) ≤ Bb) : ∀ e, GenSpec C q ad M Bb e
Context. Round six, item language: the general procedure and its correctness
genP C q (entry genE, level branch genL C, tail genTail q) is run by tabG C q ad 0 when
the descriptor register dJ holds -1 (generic mode, descriptor DescG). gen_correct: by strong
induction on the width e, tabG C q ad 0 computes progH C q e at cost costN C q Bb e V.
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_Defs13
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset
variable {W T m : ℕ} [NeZero W]
theorem IntMul.Kappa.R6.IL.gen_correct (C : Bit.QHNet (ZMod 2) W T m) (q : ℕ) (ad : IStmt HS 1) (hm : 2 ≤ m)
(hq : q.Prime) (hqB : qBound C < q) (hOK : ∀ f, C.EdgesOK (q ^ f)) (hruns : C.RunsOK)
(M Bb : ℕ) (hM : zsz (M : ℤ) ≤ Bb) : ∀ e, GenSpec C q ad M Bb e := by sorry