Abstract-real scalar algebra for the HTilde_m gradient bound (16)-(18)

Pure real-number lemmas: the geometric r₀-sum after the τ' cancellation, the elimination of 1/√ν, and the ε_{m-1}^{-(2+γ)} rpow identity. No Real.exp and no transcendental nlinarith.

theorem AVenhance.Infra.Section5.RelativeError.leh_term_eq (N Z c P t t' : ℝ) (r : ℕ) : 16 * N * (Z * t'⁻¹ ^ r) * (c * P * (8 * t) ^ (r + 1)) = 16 * N * Z * c * P * (8 * t) * (8 * t / t') ^ r

The r₀-th term, with τ'^{-r₀} cancelled against (8τ)^{r₀+1}.

theorem AVenhance.Infra.Section5.RelativeError.leh_sum_le (J : ℕ) {D x : ℝ} (hD : 0 ≤ D) (hx0 : 0 ≤ x) (hx : x ≤ 1 / 2) : ∑ r ∈ Finset.range J, D * x ^ r ≤ 2 * D

The geometric sum after the cancellation.

theorem AVenhance.Infra.Section5.RelativeError.leh_rpow_neg_sq_mul {E g : ℝ} (hE : 0 < E) : (E ^ (-(1 + g / 2))) ^ 2 * E ^ (2 + g) = 1

ε^{-(1+γ/2)} squared times ε^{2+γ} is one.

theorem AVenhance.Infra.Section5.RelativeError.leh_nu_t_L2_le {ν C a t L2 G c28 E4 : ℝ} (hC : 0 ≤ C) (ht : 0 ≤ t) (hL : 0 ≤ L2) (hν : ν ≤ C * (a * G)) (hLG : L2 * G = 1) (hat : a * t ≤ c28 * E4) : ν * t * L2 ≤ C * (c28 * E4)

The scale chain ν τ L² ≤ C 2^{-28} ε^{4δ}.

theorem AVenhance.Infra.Section5.RelativeError.leh_final_real {N c CA K S μ ν t L2 X Cn : ℝ} (hN : 0 ≤ N) (hc : 0 ≤ c) (hCA : 0 ≤ CA) (hK : 0 ≤ K) (hS : 0 ≤ S) (hμ : 0 < μ) (hμν : μ ≤ ν) (ht : 0 ≤ t) (hL : 0 ≤ L2) (hX0 : 0 ≤ X) (hX : X ≤ K * ν) (hνt : ν * t * L2 ≤ Cn) : √μ * (√2 * (2 * (128 * N * c * CA * (S / √ν) * X * t * L2))) ≤ 256 * √2 * N * c * CA * K * S * Cn

Final real chain: √μ √2 (2 D) ≤ 256 √2 N c CA K S (ν τ L²).