The layer layout has the record strides `stT` (round six, `strideSel_layer`)
ProvedNLogN.KFN.strideSel_layerThe layer layout has the record strides stT.
The following holds (Lean statement, in the scope of module Solutions.KFNSel):
theorem NLogN.KFN.strideSel_layer (hρ : ρ < K) :
StrideSel (Butterfly.layerSel P K D S ρ hρ) (fun i : Fin D => KFH.stT K D S ρ i)
Context. KFN: selected-bit operators by record strides
A selected-bit operator on a record array only needs, for every selected bit i, its record
stride st i: bit i of record j is j / st i % 2 (fbit), and setting the selected bits to
y moves to record fset st j y = j + Σ_i (y_i - bit_i) st_i. selOpF st n T xs is the
selected-bit operator in these terms.
SLaws st n: the strides are those of a genuine selected-bit structure onnrecords (fsetstays belownand reads backy).selOpF_mul,selOpF_one,selOpF_diagonal: the operator calculus.StrideSel Sb st: aSelBitsstructure whose bits/sets are given by the strides;selOp_eq_selOpFandslaws_of_strideSel.strideSel_layer: the layer layout[P] × [2^K]^D × [S]has stridesstT K D S ρ i(independent ofP).subOp g T(Ton the bitsg κ, identity elsewhere) andselOpF_subOp:selOpF st n (subOp g T) = selOpF (st ∘ g) n T. This one lemma gives reindexing (gan equivalence,subOp_tens), the child slots (slotOp_eq_subOp) and the pieces (embed_eq_subOp).
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_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFN
open AModel Matrix Finset
variable {P K D S ρ : ℕ}
theorem NLogN.KFN.strideSel_layer (hρ : ρ < K) :
StrideSel (Butterfly.layerSel P K D S ρ hρ) (fun i : Fin D => KFH.stT K D S ρ i) := by sorry