A child step from an implementation of the child level

A child step from an implementation of the child level.

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

theorem NLogN.KFW.stepQ_child {σ : Fin HS → Option ℤ} {K t S0 r H k e B Bn : ℕ}
    (hN : NodeR σ K t S0 r H k e B Bn) (hQ : ∀ s, Q s → Agree σ s) (hhi : hi ≤ H)
    (hr : 1 ≤ r) (hS : 1 ≤ S0) (hBn : 1 ≤ Bn) (hK : 1 ≤ K)
    (hKe : K * (mC ^ (k + 1) - 1) ≤ e) (het : e - e % K + K ≤ t) (Z : ℕ)
    (hZ : zsz ((16 * (P8Lift.Wc * (nN Bn t S0 * r)) : ℕ) : ℤ) ≤ Z)
    (hZe : zsz ((e + t + K + mC ^ k : ℕ) : ℤ) ≤ Z) (Bz : ℕ)
    (hBz : zsz ((k + 1 + e + mC + K * mC ^ k + ES (k + 1) + P8Lift.sc + NLogN.KFW.cL + Bn + 4 * mC ^ k + 4 :
      ℕ) : ℤ) ≤ Bz)
    {jL : Fin Pp} {rowC : IStmt HS Pp} (hj : tbl jL = levC jL rowC)
    (w : Fin P8Lift.Wc) (h : Fin mC) (fwd : Bool) (DWc : ℕ) (cIH : ℕ → ℕ)
    (IH : SImplQ Isym tbl (fun s => Agree (σChild σ K k e Bn h) s) 0 H r
      (fun c : Fin (mC ^ k) => 2 ^ ((e - h.val * (K * mC ^ k)) - K * c.val) * S0) (nN Bn t S0)
      (Butterfly.tens Cm) (levC jL rowC) (ES k) DWc cIH) :
    RImplQ Isym tbl Q lo hi r (nN Bn t S0) (stN K e k S0)
      ((P8Lift.RStep.child w h fwd : P8Lift.RStep (Fin P8Lift.Wc) mC).den
        (Butterfly.tens Cm : Butterfly.Op (Fin (mC ^ k))))
      (wrapQ P8Lift.Wc w.val wL NLogN.KFW.wP
        (withPushI (childPush h) (if fwd then .call jL else cinvU jL)))
      (ES k) (DWc + (ES k + 2) * P8Lift.Wc)
      (cWrapQ P8Lift.Wc (nN Bn t S0 * r) Z (ES k) DWc
        (fun x => cFrame 5 6 Bz + cChildF cIH (cPhZ Z Bz Bn t S0 r) DWc fwd x +
          (5 * (2 * Bz + 2) + 1)))

Context. The lemma belongs to the part KFW: level registers, the child frame, ZD passes and the uniform child step.

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.