A `±1` role diagonal (round six, `cost_fixGH`)

A ±1 role diagonal (at most W phase steps).

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

theorem IntMul.Kappa.R6.IL3H.cost_fixGH {W A m Bn t S0 r Z H F x : ℕ} (hW : 1 ≤ W) (hS : 1 ≤ S0) (hBn : 1 ≤ Bn)
    (hZ : 3 ≤ Z) (U : Finset (Fin W))
    (hx : x + ((negSteps (m := m) U.toList).map (fun _ => 0 + (0 + 2) * W)).sum ≤ H) :
    costL (phCostFH W m Z Bn t S0 r F) (fun _ => 0 + (0 + 2) * W) (negSteps (m := m) U.toList)
      x ≤ MlocH W A m * ((W * nN Bn t S0) * Yu r Z 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*).