Uniform Proposition 14 interface P14Need6 at every admissible round-six parameter record

For every round-six parameter record $P$ with $P.\mathrm{Ok}$, P14Need6 P holds: for every IL table tab with a canonical Lemma 12 code l12 (IL.L12Canon tab l12 P.τ), every complex network interface $J$ (Cx.Prop8IfaceH 207387136 T 576 Jain.cxR6) whose gates lie in the item-language gate class (IL3H.GClassH J A), if the histogram moment satisfies $\mathrm{histMoment}(\mathrm{cxR6},576,P.\sigma)<207387136$ and $2+576\log(\mathrm{histRankSum}(\mathrm{cxR6}))\le P.C_1$, then there is a guard $E_w$ with $E_w(D)\le C\,D^{C_1}$ for $D\ge1$ (EwOK6) such that the uniform Proposition 14 IL3.P14UH' tab Ew P.lamp holds.

In Lean:

theorem IntMul.Kappa.R6.IL3H.p14Need6_all (P : Prm) (hP : P.Ok) : P14Need6 P

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