The word energies of T in the twistie1 bound

From the three gradient contracts (‖∇ ∂^w T‖, |w| ≤ 2, at the rate L) to the bound of the sum U = ∑_w 14336 D² L^{2(2-|w|)} ‖∇ ∂^w T‖²_{L²((0,1)×𝕋²)} of se_time_bound.

theorem AVenhance.Infra.Section5.Contracts.se_U_le {κp L A Bm CB1 : ℝ} (hκp : 0 < κp) (hCB1 : 0 ≤ CB1) (hAB : 0 ≤ A * Bm) (S : List (Fin 2) → ℝ) (hS0 : ∀ w ∈ scWords2, 0 ≤ S w) (hS : ∀ w ∈ scWords2, √κp * √(S w) ≤ A * Bm * L ^ w.length) : √(∑ w ∈ scWords2, 14336 * (κp * CB1) ^ 2 * (L ^ (2 - w.length)) ^ 2 * S w) ≤ √100352 * (CB1 * A * Bm * L ^ 2) * √κp