A child call (forward or inverse) from the level-k claim

A child call (forward or inverse) from the level-k claim.

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

theorem NLogN.KFN.step_child {k Ek DWk Wk : ℕ} {ck : ℝ} (IH : Lv Isym iprog K W m r Z Ψ k Ek DWk Wk ck) (G : ℝ)
    (hG : 0 ≤ G) (hW : 1 ≤ W) (hr : 1 ≤ r) (hΨm : Monotone Ψ) (hZΨ : ∀ v, Z + 2 ≤ Ψ v)
    (pos : Fin m × Fin (m ^ k) → ℕ) (hinj : Function.Injective pos) {t S0 B : ℕ}
    (hpos : ∀ p, pos p < t) (haff : AffK2 K t m k pos) (hS : 1 ≤ S0) (hB : 1 ≤ B)
    (hdvd : W ^ k ∣ B)
    (hZ : zsz ((16 * (W * nR t S0 B * r)) : ℕ) ≤ Z) (w0 : Fin W) (h : Fin m) (fwd : Bool)
    (O : ℕ) (hO : DWk + (Ek + 2) * W + Ek + 4 ≤ O) :
    ∃ (code : ℕ → IStmt HS Pp) (e dw : ℕ) (cost : ℕ → ℕ),
      RImplI Isym iprog r (nR t S0 B) (fun p => 2 ^ pos p * S0)
        ((RStep.child w0 h fwd : RStep (Fin W) m).den (Butterfly.tens Cm)) code e dw cost ∧
      e ≤ Ek ∧ dw ≤ DWk + (Ek + 2) * W ∧ ∀ w, (cost w : ℝ) ≤
        ck * ((nR t S0 B : ℕ) : ℝ) * (Xf r Ψ (w + Wk) : ℝ) +
        ((alN W A : ℝ) + G) * ((W * nR t S0 B : ℕ) : ℝ) * (Xf r Ψ (w + O) : ℝ)

Context. The lemma belongs to the part KFN: the steps of a node at level k+1, with bounds: Node bits Fin m × Fin (m^k) at strides 2^{pos p} S₀, W roles of n = B · 2^t · S₀ records each. step_ok: every step of J.net has an implementation (RImpl) with

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.