arrInv_step (KFY 16: the `A` pass and the `B₀` pass)

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

theorem NLogN.KFY.arrInv_step {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n) (k : ℕ) (hk : k < IntMul.OpenAI.Glue.dP n)
    (f : List KFB.GI → List KFB.GI)
    (hf : ∀ X : List KFB.GI, X.length = tN n k → (f X).length = tN n k)
    (hd : ∀ X, DiscL (IntMul.OpenAI.Glue.pP n) X → DiscL (IntMul.OpenAI.Glue.pP n) (f X)) (X : List KFB.GI)
    (hX : ArrInv n X) : ArrInv n (stepL ((List.ofFn (KFM.tB n)).rotate k) f X)

Context. The lemma belongs to the part KFY 16: the A pass and the B₀ pass: The arrays keep the invariant length = ∏ t_i, DiscL p (which gives GB (p + 2)), using an M : AxisMaps (disc_sapL, disc_b0Pad).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.