The node inequality (round six, `Gs_node`)

The node inequality.

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

theorem IntMul.Kappa.R6.IL3H.Gs_node {A p m c E : ℕ} (ws : List ℕ) (hm : 1 ≤ m) (hp : 1 ≤ p) (hA : 2 * c + 1 ≤ A)
    (hE : 2 * m ≤ E) (hws : 2 * (ws.map fun s => (2 * s + 1) ^ p).sum ≤ (2 * m) ^ p) :
    c + (ws.map fun s => Gs A p m (s * (E / m))).sum + Gs A p m (E % m) ≤ Gs A p m E

Context. Round six, item language (I3): the network in the item-language numbering

• mapR e: transport of a step along a role equivalence; denListH_mapR: the denotation is reindexed.
• netF J: the normalized network (R6IL3Norm) with roles Fin (W + T) (data first, roleEqv); netF_child (children are forward prefix children of width < m), netF_gate (gate class), netF_data (the data-to-data block is C^{⊗} on every data role), netF_widths.
• Gs A p m x: the closed-form scale bound (x below 2m, A((x+1)^p - 1) above); Gs_node: a node on E = mF + r ≥ 2m bits whose children have widths s F (s in ws, 2 Σ (2s+1)^p ≤ (2m)^p) has local scale c plus child scales plus leftover scale at most Gs E.
• dep m x: the number of node levels below x bits (dep_child, dep_mono).

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