Round six: normalization of the CrudeAssembly hypotheses to a parameter record

Let $a_b, a_c \ge 0$ be the savings of S. Jain's round-six bit and complex networks, i.e. assume the moment bounds

where $\mu_\tau(h; m) = \sum_{(w,n_w) \in h} n_w\,(w/m)^{\tau}$ is the moment of the child-width histograms $h_{\mathrm{bit}} =$ Jain.bitR6, $h_{\mathbb C} =$ Jain.cxR6 (from Def_IntMul_KappaJainData). Assume further the crude-assembly constraints CrudeAssembly $(a_b, a_c, \beta = 1/1000, \varepsilon, x, C_1, \kappa, 576, s_c)$ of the κ framework, with $s_c$ the rank sum of $h_{\mathbb C}$.

Then there is a parameter record $P = (\tau, \sigma, \varepsilon', \lambda', x', C_1')$ with $P$ satisfying all the constraints Prm.Ok (in particular $1/2 \le \varepsilon' < 1$, $0 < \tau, \sigma \le 1$, natural $x' \ge 1$), with $\kappa < \mathrm{gap}(P)$ (the minimum of the five cost margins), with the two moment bounds holding at the exponents $\tau = P.\tau$ and $\sigma = P.\sigma$, and with the depth-guard condition

This is the first step of the round-six argument: all later statements are parametrized by such a record $P$, and the reduction to $\varepsilon \ge 1/2$ means only one cost regime has to be treated.

In Lean:

theorem IntMul.Kappa.R6.r6_normalize (ab ac ε x C₁ κ : ℝ) (hab : 0 ≤ ab) (hac : 0 ≤ ac)
    (hbit : histMoment Jain.bitR6 529 (1 - ab) < 148225616)
    (hcx : histMoment Jain.cxR6 576 (1 - ac) < 207387136)
    (hasm : CrudeAssembly ab ac (1 / 1000) ε x C₁ κ 576 (histRankSum Jain.cxR6)) :
    ∃ P : Prm, P.Ok ∧ κ < P.gap ∧ histMoment Jain.bitR6 529 P.τ < 148225616 ∧
      histMoment Jain.cxR6 576 P.σ < 207387136 ∧
      2 + 576 * Real.log (histRankSum Jain.cxR6) ≤ P.C1

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