Every step of a node

Every step of a node.

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

theorem NLogN.KFW.step_any {rowC : IStmt HS Pp} {Kc : ℝ} (hRow : RowU Isym tbl rowC Kc) (hKc : 0 ≤ Kc)
    {jL : Fin Pp} (hj : tbl jL = levC jL rowC)
    (hN : NodeR σ K t S0 r H k e B Bn) (hB : B = P8Lift.Wc * Bn)
    (hK6 : 6 ≤ K) (hr : 1 ≤ r) (hKZ : 80 * Z * (Z + 2) ≤ 2 ^ K) (Zr : ℕ) (hZZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r)
    (hHZ : H + 1 < 2 ^ Z) (hS : 1 ≤ S0) (hBn : 1 ≤ Bn)
    (hKe : K * (mC ^ (k + 1) - 1) ≤ e) (het : e - e % K + K ≤ t)
    (hz16 : zsz ((16 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Z)
    (hV : zsz ((Vb K t S0 r H (k + 1) B : ℕ) : ℤ) ≤ Zr) (cI : ℕ)
    (IH : ∀ h : Fin mC, 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) (DWb Lc P8Lift.sc P8Lift.Wc NLogN.KFW.A0 k) (fun _ => cI))
    (a : P8Lift.RStep (Fin P8Lift.Wc) mC) (ha : a ∈ P8Lift.complexIface.net) :
    ∃ (dw c : ℕ), RImplQ Isym tbl (fun s => Agree σ s) 0 H r (nN Bn t S0) (stN K e k S0)
        (a.den (Butterfly.tens Cm)) (stepC jL rowC a) (eSt k a) dw (fun _ => c) ∧
      dw ≤ (if a.isChild then DWb Lc P8Lift.sc P8Lift.Wc NLogN.KFW.A0 k + (Eb Lc P8Lift.sc k + 2) * P8Lift.Wc
        else dwloc P8Lift.Wc NLogN.KFW.A0) ∧
      (c : ℝ) ≤ (if a.isChild then (cI : ℝ) else 0) +
        ((Mloc : ℝ) + 18 * (Kc * (K + 2) + 1) * ((mC : ℝ) ^ k + 1) ^ τ50) *
          ((P8Lift.Wc * nN Bn t S0 * Yu r Zr H : ℕ) : ℝ)

Context. The lemma belongs to the part KFW: the steps of a node of the uniform level procedure.

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.