The cost recurrence (round six, `cH_rec`)

The cost recurrence. For e ≥ m, c(e) = (e mod m) + K₀ + (1/W) Σ_w c(w ⌊e/m⌋), the sum over all children (C.widths).

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

theorem IntMul.Kappa.R6.Bit.cH_rec (C : QHNet R W T m) (hruns : C.RunsOK) {e : ℕ} (he : m ≤ e) :
    cH C e = ((e % m : ℕ) : ℝ) + K0 C + (C.widths.map fun w => cH C (w * (e / m))).sum / W

Context. Round six, bit side: cost of progH and the generalized Prop. 11

costH C e V: the structural cost of progH C q e … on an array of volume V, following the program: e < m: e digit-swap passes; e = m f + r: r digit-swap passes, the row split and merge (2V), T zero temporaries (T V / W), each gate one pass per touched wire (V / W), each edge 4m shift passes (V / W each) plus its run children, each a recursive call of width r' f on a stream of volume V / W.

• costH_lin: costH e V = V · costH e 1.
• cH_rec: c(e) = (e mod m) + K₀ + (1/W) Σ_{children} c(w ⌊e/m⌋) (c = costH · 1).
• costH_bound: with histMoment C.hist m τ < W, costH e V ≤ K V e^τ for all e (via the monotone majorant of c and R6.MomentRec.moment_recurrence_bound).
• prop11H: denotation and cost together.

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