Local work (round six, `locWork_le_vol`)

Local work ≤ nloc · (W+T) · |states|, i.e. ≤ (nloc (W+T)²/W) · V with the data volume V = W · 2^{m|κ|}.

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

theorem IntMul.Kappa.R6.Cx.Prop8IfaceH.locWork_le_vol (J : Prop8IfaceH W T m h) (κ : Type) [Fintype κ]
    [DecidableEq κ] :
    (J.locWork κ : ℝ) ≤ ((J.net.filterMap HStep.locR).length * ((W + T : ℕ) : ℝ) ^ 2 / W) *
      (W * 2 ^ (m * Fintype.card κ))

Context. R2: cost of the recursive C-layer through a Prop8IfaceH network (moment recurrence)

Cost model (§5.3, as Butterfly.recCost, now on any number of axes e = m f + r): a node on e ≥ m axes and data volume V costs Lloc · V for the local steps of one network invocation (locWork_le_vol: Lloc = nloc (W+T)²/W bounds the actual entry operations), r · V for the r = e mod m leftover individual kernels, and one recursive call on |S| f axes and volume V / W per child; a leaf (e < m) costs e · V (individual kernels).

• recCostH_lin: recCostH e V = V · recCostH e 1.
• recCostH_unit_node: the per-volume recurrence c(e) = Lloc + r + (1/W) ∑_w n_w c(w f).
• recCostH_le: if ∑_w n_w (w/m)^σ < W (histMoment h m σ < W), then recCostH e V ≤ K · V · e^σ for all e, V ≥ 0 (via moment_recurrence_bound applied to the running maximum of c).

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