A node level (round six, `sImplQ_nodeC`)

A node level.

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

theorem IntMul.Kappa.R6.IL3H.sImplQ_nodeC {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)
    (hL : LevRH 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) (hE2 : 2 * c.m ≤ E) (hW1 : 1 ≤ c.W)
    (hWB : c.W ∣ B) (hB1 : 1 ≤ B)
    (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)
    (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 * (E - 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 + cLH c + B + c.W + S0 + r + K +
      S0 * r + K * E + e + 1 ≤ M)
    (hMZ : zsz (M : ℤ) ≤ Zr)
    (hzA : zsz ((2 * (c.Wr * (nN (B / c.W) t S0 * r)) + 16 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Zr)
    (hGH : c.G E ≤ H)
    (hδ : cLH c + ((chWs c).map fun s => c.G (s * (E / c.m))).sum + E % c.m ≤ c.G E)
    (DWc cI : ℕ → ℕ)
    (IHc : ∀ s, s < c.m →
      SImplQ Isym tbl (fun s' => Agree (σChildH (σNodeH σ c K t S0 r E B) 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))
    (DWR cR : ℕ)
    (IHR : SImplQ Isym tbl (fun s => Agree (σPush (σNodeH σ c K t S0 r E B)
        (frV (σNodeH σ c K t S0 r E B) (leftFr c))) s) 0 H r
      (fun j : Fin (E % c.m) => 2 ^ ((e - K * (c.m * (E / c.m))) - K * j.val) * S0) (nN B t S0)
      (tens Cm) (levCH c jL rowC) (c.G (E % c.m)) DWR (fun _ => cR)) :
    ∃ cost : ℕ → ℕ, SImplQ Isym tbl (fun s => Agree σ s) 0 H r
      (fun i : Fin E => 2 ^ (e - K * i.val) * S0) (nN B t S0) (tens Cm) (IntMul.Kappa.R6.IL3H.nodeC c jL rowC)
      (c.G E) ((c.net.map (dwStH c DWc (E / c.m))).sum + (DWR + (δv c E + 2) * 2)) cost ∧
      ∀ w, w + ((c.net.map (dwStH c DWc (E / c.m))).sum + (DWR + (δv c E + 2) * 2)) ≤ H →
        (cost w : ℝ) ≤ (((chWs c).map cI).sum : ℝ) + (cR : ℝ) +
          ((c.net.length : ℝ) * ((MH c : ℝ) + 18 * aK K *
            (((E / c.m : ℕ) : ℝ) + 1) ^ τ) + (CnN c : ℝ)) *
          ((c.Wr * nN (B / c.W) t S0 * Yu r Zr H : ℕ) : ℝ)

Context. Round six, item language (I3): a node level

sImplQ_nodeC: for E ≥ 2m, nodeC c jL rowC (node frames, the steps of the network, the leftover call, the scale pad) implements tens Cm on the E bits, scale Gs E, width ∑ dwStH + DWR + 2 (δ + 2), at cost ≤ ∑_{children s} cI s + cR + (L (MH + Γ_F) + CnN) · W' n' Y.

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*).