An operator on a subfamily of the selected bits is the operator with the restricted strides

An operator on a subfamily of the selected bits is the operator with the restricted strides.

The following holds (Lean statement, in the scope of module Solutions.KFNSel):

theorem NLogN.KFN.selOpF_subOp {g : κ → ι} (hg : Function.Injective g) (st : ι → ℕ) (n : ℕ)
    (T : Matrix (κ → Fin 2) (κ → Fin 2) ℂ) (xs : List M) :
    selOpF st n (subOp g T) xs = selOpF (st ∘ g) n T xs

Context. The lemma belongs to the part 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.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs20.