Pure real arithmetic for the relative dissipation step. All transcendental quantities are supplied as abstract scalars to the polynomial arguments.

theorem AVenhance.Infra.Section5.RelativeError.relative_sqrt_square_gap {u v B : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hB : 0 ≤ B) (h : |u ^ 2 - v ^ 2| ≤ B ^ 2) : |u - v| ≤ B

theorem AVenhance.Infra.Section5.RelativeError.relative_energy_gap_of_norm_gap {u S K e : ℝ} (hu : 0 ≤ u) (hS : 0 ≤ S) (hK : 0 ≤ K) (he : 0 ≤ e) (he1 : e ≤ 1) (h : |u - S| ≤ K * e * S) : |u ^ 2 - S ^ 2| ≤ K * (2 + K) * e * S ^ 2