Generalized Prop. 11, cost (round six, `costH_bound`)

Generalized Prop. 11, cost. If every run is valid and Σ n_w (w/m)^τ < W, the program costs O(V e^τ) for every width e.

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

theorem IntMul.Kappa.R6.Bit.costH_bound (C : QHNet R W T m) (hruns : C.RunsOK) (hm : 2 ≤ m) {τ : ℝ} (hτ0 : 0 < τ)
    (hτ1 : τ ≤ 1) (hmom : histMoment C.hist m τ < W) :
    ∃ K : ℝ, ∀ (e : ℕ) (V : ℝ), 0 ≤ V → costH C e V ≤ K * V * (e : ℝ) ^ τ

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