Round six, complex side: correctness and cost of the recursive C-layer for slot-set networks

Let $J$ be a round-six complex interchange network Prop8IfaceH W T m h: a program on $W$ data roles and $T$ clean temporaries whose recursive child calls act on slot sets $S \subseteq \{0,\dots,m-1\}$ (with sign sets), whose child widths form the multiset described by the histogram $h = [(w, n_w)]$, and which is correct on the data-to-data block. Let $m \ge 2$, $0 < \sigma \le 1$, $L_{\mathrm{loc}} \ge 0$, all widths $0 < w < m$, and assume the moment condition

Then (1) for every number of axes $e$, the recursive C-layer recOpH J e computes exactly $C^{\otimes e}$, and (2) there is a constant $K$ such that its cost on volume $V \ge 0$ satisfies

This is the complex-side analogue of the OpenAI network recursion (§5.3), extended to children of arbitrary widths via slot sets.

In Lean:

theorem IntMul.Kappa.R6.Cx.recH_main {W T m : ℕ} {h : List (ℕ × ℕ)} [NeZero W] (J : Prop8IfaceH W T m h)
    {Lloc σ : ℝ} (hL : 0 ≤ Lloc) (hm : 2 ≤ m) (hσ0 : 0 < σ) (hσ1 : σ ≤ 1)
    (hw : ∀ p ∈ h, 0 < p.1 ∧ p.1 < m) (hmom : IntMul.Kappa.histMoment h m σ < W) :
    (∀ e, recOpH J e = Butterfly.tens Butterfly.Cm) ∧
      ∃ K : ℝ, ∀ (e : ℕ) (V : ℝ), 0 ≤ V → recCostH J Lloc e V ≤ K * V * (e : ℝ) ^ σ

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