The child wrapper (round six, `cost_childH`)

The child wrapper overhead (constant child cost cI).

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

theorem IntMul.Kappa.R6.IL3H.cost_childH {c : IntMul.Kappa.R6.IL3H.Cfg} {W A m Bn t S0 r Z Zr H G DWc x cI : ℕ} (hW : 1 ≤ W)
    (hZZ : Z ≤ Zr) (hS : 1 ≤ S0) (hBn : 1 ≤ Bn) (hsz : gsSz c + 6 ≤ A) (hGH : G ≤ H)
    (hGZ : zsz (G : ℤ) ≤ Zr) (hZr : Zr + 2 ≤ r) (hx : x + (DWc + (G + 2) * W) ≤ H) :
    cChF c Zr G + cWrapQ W (nN Bn t S0 * r) Z G DWc (fun _ => cI + 2) x +
      (4 * (2 * (Zr + G + 1) + 2) + 1) ≤ cI + MlocH W A m * ((W * nN Bn t S0) * Yu r Zr H)

Context. Round six, item language (I3): cost bounds of the steps of a node

KFWCost2 with the literal W_c, A0, mC replaced by variables: with P = (W n) · Yu r Z H (n records per role, W roles, at most A atoms per gate, m slots):

• cost_gateH, cost_permH, cost_phaseH, cost_fixGH, cost_rowH: every local step costs ≤ MlocH W A m · P (plus the row body);
• cost_childH: the child wrapper adds ≤ MlocH W A m · P to the (constant) child cost, for gsSz c + 6 ≤ A.

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