Inductive step of the generalized Prop. 11 (round six, `levelH_correct`)
ProvedIntMul.Kappa.R6.Bit.levelH_correctInductive step of the generalized Prop. 11. With exact children and C.OK N, one level
is the interchange of the two chunks (block swap of the two runs of m fields).
The following holds (Lean statement, in the scope of module Solutions.R6BitLevel):
theorem IntMul.Kappa.R6.Bit.levelH_correct (hOK : C.OK N) {child : ℕ × ℕ × ℕ → List R → List R}
(hch : ChildOKH (R := R) (m := m) N P L' A B Cs child) {xs : List R}
(_hxs : xs.length = vol (P :: W * L' :: hdShape A B Cs m N)) :
levelH C N P L' A B Cs child xs =
pull (P :: W * L' :: hdShape A B Cs m N) (P :: W * L' :: hdShape A B Cs m N)
(blockSwap (A.length + 2) (A.length + B.length + m + 2) m) 0 xs
Context. Round six, bit side: one level of the generalized Prop. 11
On the shape P :: (W L') :: hdShape A B Cs m N (two chunks of m fields of size N):
split the rows into W role streams (plus T zero temporaries), run the network with every
edge implemented by its shifts and one child call per run (realEdge), merge back undoing
ρ. With correct children and C.OK N this is the chunk interchange (levelH_correct).
realEdge_eq: with children equal to the exact run transpositions, the implemented edge is the ideal one (runArrof the Bruhat steps).runArr_runPiv: on the stream layout, the transpositions of a run(i, j, r)are the block swap of the field runsH_i … H_{i+r-1}andD_j … D_{j+r-1}.levelH_correct.
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] {m : ℕ}
variable {W T : ℕ} [NeZero W] (C : QHNet R W T m) (N P L' : ℕ) (A B Cs : Shape)
variable [NeZero N]
theorem IntMul.Kappa.R6.Bit.levelH_correct (hOK : C.OK N) {child : ℕ × ℕ × ℕ → List R → List R}
(hch : ChildOKH (R := R) (m := m) N P L' A B Cs child) {xs : List R}
(_hxs : xs.length = vol (P :: W * L' :: hdShape A B Cs m N)) :
levelH C N P L' A B Cs child xs =
pull (P :: W * L' :: hdShape A B Cs m N) (P :: W * L' :: hdShape A B Cs m N)
(blockSwap (A.length + 2) (A.length + B.length + m + 2) m) 0 xs := by sorry