The closed form satisfies the cost recursion (round six, `cbRec_of`)

The closed form satisfies the cost recursion.

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

theorem IntMul.Kappa.R6.IL3H.cbRec_of {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) {aK : ℕ → ℝ} {τ θ : ℝ} {K : ℕ} (haK : 0 ≤ aK K)
    (hτ : 0 ≤ τ) (hτθ : τ ≤ θ) (Cc D0 : ℝ) (hCc0 : 0 ≤ Cc)
    (hD0 : D0 = 10 ^ 14 * (2 * c.m + 1))
    (hCc : ((chWs c).length : ℝ) * D0 + 18 * c.Wr * c.net.length * 2 ^ τ + C1H c ≤
      Cc * ((c.W : ℝ) - momH c θ)) :
    CBRec c aK τ K (CBH c.m (aK K + 1) Cc D0 θ)

Context. Round six, item language (I3): closed-form cost coefficients

CBH E = (aK K + 1) · Φ(E) with Φ(E) = 10^14 (E + 1) on the chain levels E < 2m and Φ(E) = Cc E^θ + D0 on the node levels. cbRec_of: CBH satisfies the cost recursion CBRec when τ ≤ θ, the θ-moment α = ∑_{children} (s/m)^θ < W holds, D0 = 10^14 (2m+1) and Cc (W - α) ≥ nC D0 + 18 W' L 2^τ + C1 (C1 = W' (L MH + CnN + 10^12)).

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