The interior of a node (round six, `sImplQ_nodeIn`)

The interior of a node.

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

theorem IntMul.Kappa.R6.IL3H.sImplQ_nodeIn {rowC : IStmt HS Pp} {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC)
    (hN : NodeRH c σ K t S0 r H E e B) (hok : NetOK c) (hm : 1 ≤ c.m) (hE2 : 2 * c.m ≤ E)
    (hW1 : 1 ≤ c.W) (hWB : c.W ∣ B) (hB1 : 1 ≤ B) (hK : 1 ≤ K) (hS : 1 ≤ S0) (hr : 1 ≤ r)
    (hKe : K * (E - 1) ≤ e) (het : e - e % K + K ≤ t) (Zr : ℕ)
    (hzA : zsz ((2 * (c.Wr * (nN (B / c.W) t S0 * r)) + 4 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Zr)
    (hZr : Zr + 2 ≤ r)
    (M : ℕ) (hM : E + e + K * E + K + c.m + 1 ≤ M) (hMZ : zsz (M : ℤ) ≤ Zr)
    (dwf cf : HStep (Fin c.Wr) c.m → ℕ)
    (hP : ∀ a ∈ c.net, 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) (dwf a) (fun _ => cf a))
    (DWR cR : ℕ)
    (IHR : SImplQ Isym tbl (fun s => Agree (σPush σ (frV σ (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)
      (.seq (padCU 23 21 (seqLQ (IntMul.Kappa.R6.IL3H.stepH c jL rowC) c.net))
        (.seq (withPushI (fr (leftFr c)) (.call jL)) (scaleQ 23 23 25 26)))
      ((c.net.map (eStH c (E / c.m))).sum + (c.G (E % c.m) + δv c E))
      ((c.net.map dwf).sum + (DWR + (δv c E + 2) * 2)) cost ∧
      ∀ w, w + ((c.net.map dwf).sum + (DWR + (δv c E + 2) * 2)) ≤ H →
        cost w ≤ (c.net.map cf).sum + cR + 10 ^ 17 * (c.Wr * nN (B / c.W) t S0 * Yu r Zr H)

Context. Round six, item language (I3): the interior of a node

Under a node assignment (NodeRH), given implementations of the steps of the network (constant costs cf a, widths dwf a) and of the leftover call (cost cR, width DWR), the interior of nodeC

padCU 23 21 (steps) ; (leftover frame; call jL) ; scaleQ 23 23 25 26

implements tens Cm on the E bits (scale ∑ eStH + (Gs (E mod m) + δ)), with cost ≤ ∑ cf + cR + 10^17 · W' n' Y on the whole window (sImplQ_nodeIn).

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