Every step of a node (round six, `step_anyH`)

Every step of a node.

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

theorem IntMul.Kappa.R6.IL3H.step_anyH {rowC : IStmt HS Pp} {aK : ℕ → ℝ} {τ : ℝ} {G : ℕ}
    (hRow : RowUCG c.m τ Isym tbl rowC aK G)
    (haK : ∀ K, 0 ≤ aK K) (hτ : 0 ≤ τ) {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC) (hok : NetOK c)
    (hN : NodeRH c σ K t S0 r H E e B) (hG24 : σ vG = some (G : ℤ))
    (hA : 1 ≤ c.Aw) (hp : 1 ≤ c.p) (hm : 1 ≤ c.m) (hF : 1 ≤ E / c.m) (hW : 1 ≤ c.Wr)
    (hK6 : 6 ≤ K) (hr : 1 ≤ r) {Z : ℕ} (hZG : 4 * Z * (Z + 2) ≤ 2 ^ G)
    (hGK : 16 * Z * (Z + 2) * 2 ^ G ≤ 2 ^ K) (Zr : ℕ) (hZZ : Z ≤ Zr)
    (hZr : Zr + 2 ≤ r) (hHZ : H + 1 < 2 ^ Z) (hS : 1 ≤ S0) (hBn : 1 ≤ B / c.W)
    (hdB : 2 ^ (2 * ((E / c.m - 1) * G)) ∣ B / c.W) (hdS : 2 ^ ((E / c.m - 1) * G) ∣ S0)
    (hGz : zsz (G : ℤ) ≤ Zr)
    (hKe : K * (c.m * (E / c.m) - 1) ≤ e) (het : e - e % K + K ≤ t)
    (hz16 : zsz ((16 * (c.Wr * (nN (B / c.W) t S0 * r)) : ℕ) : ℤ) ≤ Z)
    (hze : zsz ((e + t + K + c.m * (E / c.m) + E / c.m : ℕ) : ℤ) ≤ Zr)
    (hzu : zsz ((6 * (E / c.m) + 6 : ℕ) : ℤ) ≤ Zr)
    (hzrow : zsz ((E / c.m + K + e + t + S0 + B / c.W + r + H + c.m : ℕ) : ℤ) ≤ Zr)
    (hz3 : 3 ≤ Zr) (M : ℕ)
    (hM : c.Aw * (E + 1) ^ c.p + (E + 1) ^ c.p + E + 2 * c.m + B + 1 ≤ M)
    (hMZ : zsz (M : ℤ) ≤ Zr) (hGH : c.G E ≤ H)
    (DWc cI : ℕ → ℕ)
    (IH : ∀ s, s < c.m → SImplQ Isym tbl (fun s' => Agree (σChildH σ c s (E / c.m) (B / c.W)) s')
      0 H r (fun i : Fin (s * (E / c.m)) => 2 ^ (e - K * i.val) * S0) (nN (B / c.W) t S0)
      (tens Cm) (levCH c jL rowC) (c.G (s * (E / c.m))) (DWc s) (fun _ => cI s))
    (a : HStep (Fin c.Wr) c.m) (ha : a ∈ c.net) :
    ∃ (dw cc : ℕ), RImplQ Isym tbl (fun s => Agree σ s) 0 H r (nN (B / c.W) t S0)
        (stH c.m K e (E / c.m) S0) (a.den (chEx (κ := Fin (E / c.m)))) (IntMul.Kappa.R6.IL3H.stepH c jL rowC a)
        (eStH c (E / c.m) a) dw (fun _ => cc) ∧
      dw ≤ dwStH c DWc (E / c.m) a ∧
      (cc : ℝ) ≤ (chCostH cI a : ℝ) +
        ((MH c : ℝ) + 18 * aK K * (((E / c.m : ℕ) : ℝ) + 1) ^ τ) *
          ((c.Wr * nN (B / c.W) t S0 * Yu r Zr H : ℕ) : ℝ)

Context. Round six, item language (I3): every step of a node

• NetOK c: what the level procedure needs from the network c.net (gate class, normalized children, the data block of its operator);
• eStH: the scale of a step; sum_eStH: the steps of a node have total scale cLH c + ∑_{children} Gs (s F);
• rImplQ_listH: a list of implemented HSteps implements denListH;
• step_anyH: every step of c.net at a node on E bits, coded by stepH, has an implementation with constant cost ≤ (child cost) + (MlocH + 18 CR (F+1)^τ) · W n · Yu.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).