I1: uniform swaps for any round-six bit network (round six, `swapNeedtau_of_net`)

I1: uniform swaps for any round-six bit network, cost K (w+1)(V+1) u^τ plus the descriptor term, τ any exponent with Σ n_w (w/m)^τ < W.

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

theorem IntMul.Kappa.R6.IL.swapNeedtau_of_net {W T m : ℕ} [NeZero W] (C : Bit.QHNet (ZMod 2) W T m) (hC : NetIL C)
    {τ : ℝ} (hτ0 : 0 < τ) (hτ1 : τ ≤ 1) (hmom : histMoment C.hist m τ < W) :
    ∃ (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1), L12Canon tab l12 τ ∧ SwapNeedτ tab τ

Context. Round six, item language: item I1 (swapNeedτ_of_net)

For every round-six bit network C : QHNet (ZMod 2) W T m with NetIL C and every exponent τ ∈ (0, 1] with Σ n_w (w/m)^τ < W (histMoment C.hist m τ < W) there is a Lemma 12 table tab and code l12 with L12Canon tab l12 τ, hence SwapNeedτ tab τ (uniform axis swaps on Gaussian arrays at cost K (w+1)(V+1) u^τ plus the descriptor term) for the merged table kTableP tab.

• L12Canon → SwapNeedτ: R6ILSwapU.swapNeedτ_of_l12Canon (complete).
• ILProp11 → L12Canon: R6IL12.l12Canon_of_IL (complete), wrapper KFE.l12F q m (W ^ cW).
• ilProp11_of_net: the item-language Prop. 11 program for QHNet (R6ILProp).

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