The round-six uniform Proposition 14, explicit-hypothesis form (round six, `p14UH_prime_of`)

The round-six uniform Proposition 14, explicit-hypothesis form.

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

theorem IntMul.Kappa.R6.IL3H.p14UH_prime_of (c : IntMul.Kappa.R6.IL3H.Cfg) (hc : CfgOK c) {τ θ Cc lamp : ℝ} (hτ0 : 0 ≤ τ) (hτθ : τ ≤ θ)
    (hθl : θ ≤ lamp) (hl1 : lamp ≤ 1) (hCc0 : 0 ≤ Cc)
    (hCc : ((chWs c).length : ℝ) * (10 ^ 14 * (2 * c.m + 1)) + 18 * c.Wr * c.net.length * 2 ^ τ +
      C1H c ≤ Cc * ((c.W : ℝ) - momH c θ))
    (tab : Fin 1 → IStmt HS 1) (hrow : RowUCCP c.m τ tab) : P14UH' tab (EwH c) lamp

Context. Round six, item language (I3): the uniform Proposition 14 with explicit size hypotheses

p14UH'_of: for a configuration c (CfgOK c), exponents 0 ≤ τ ≤ θ ≤ lamp ≤ 1, a level constant Cc with the moment condition of cbRec_of, and compact-control row additions RowUCCP c.m τ tab in every extension of kTableP tab, the uniform Proposition 14 P14UH' tab (EwH c) lamp holds, with K₀ = K0c c = 2^{Zc c} and C₀ = C0c c Kc Cc.

The procedure list UUH places the level procedure (0), the kernel loop (1), the size loop (2), the field-width loop (3), the depth loop with the core and the body (4), the entry (5), and then the row procedures.

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