Abstract real inequalities for the pointwise bounds of the twistie4, twistie5 fluxes

Pure real algebra (no transcendental functions): the final squaring steps of sd_flux_bound and sd_slow_pointwise.

theorem AVenhance.Infra.Section5.Contracts.scf_flux_sq {v : Homogenization.Vec 2} {e P gT C : ℝ} (hC : 2 * C ^ 2 ≤ 64 ^ 2) (h : ∀ (i : Fin 2), |v i| ≤ C * (e * P * gT)) : Homogenization.vecNormSq v ≤ (64 * (e * P)) ^ 2 * gT ^ 2

theorem AVenhance.Infra.Section5.Contracts.scf_slow_abs {ξ K S B : ℝ} (hξ0 : 0 ≤ ξ) (hξ1 : ξ ≤ 1) (hK : 0 ≤ K) (hS : |S| ≤ B) : |ξ * K * S| ≤ K * B

theorem AVenhance.Infra.Section5.Contracts.scf_slow_abs' {ξ S B : ℝ} (hξ0 : 0 ≤ ξ) (hξ1 : ξ ≤ 1) (hS : |S| ≤ B) : |ξ * S| ≤ B

theorem AVenhance.Infra.Section5.Contracts.scf_slow_sq {f K e q gT h0 h1 : ℝ} (hK : 0 ≤ K) (he : 0 ≤ e) (hq : 0 ≤ q) (hg : 0 ≤ gT) (h0n : 0 ≤ h0) (h1n : 0 ≤ h1) (hf : |f| ≤ K * e * (4 * h0 + 4 * h1 + 16 * (2 ^ 16 * q) * gT)) : f ^ 2 ≤ (28 * 2 ^ 16 * K * e * q) ^ 2 * gT ^ 2 + (7 * K * e) ^ 2 * (h0 ^ 2 + h1 ^ 2)

The squaring step of the slow factors: with K = κ or 1, q = ε_{m-1}⁻¹.