Abstract-real scale arithmetic for the centered normie3 bound

Pure real-variable facts (no nlinarith near transcendentals):

• n3_scale1: y (1 + ψ/κ) ≤ M₁ ρ ε^δ from ψ/κ ≤ K y^{-γ}, y ≤ K x^q, 1 + γ/2 + δ ≤ q (1 - γ) (the exponent identity q(1-γ) - 1 - γ/2 = 4δ), ρ = x^{1+γ/2};
• n3_exp_scale: (1 + ψ/κ) ρ⁻² e^{-ρN/(4096 c₂)} ≲ x^δ;
• n3_arith_final: assembly of the four terms into C ε^δ √κ B.

theorem AVenhance.Infra.Section5.Contracts.n3_exponent {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 + gamma β / 2 + delta β ≤ q β * (1 - gamma β)

The exponent inequality 1 + γ/2 + δ ≤ q (1 - γ) (indeed 1 + γ/2 + 4δ = q(1-γ)).

theorem AVenhance.Infra.Section5.Contracts.n3_scale1 {x y ψκ K q γ δ : ℝ} (hx : 0 < x) (hx1 : x ≤ 1) (hy : 0 < y) (hy1 : y ≤ 1) (hyK : y ≤ K * x ^ q) (hK : 1 ≤ K) (hγ0 : 0 ≤ γ) (hγ1 : γ ≤ 1) (hψκ : ψκ ≤ K * y ^ (-γ)) (hexp : 1 + γ / 2 + δ ≤ q * (1 - γ)) : y * (1 + ψκ) ≤ (1 + K) * K * (x ^ (1 + γ / 2) * x ^ δ)

theorem AVenhance.Infra.Section5.Contracts.n3_exp_scale {γ δ : ℝ} (hγ0 : 0 ≤ γ) (hγ1 : γ ≤ 1) (hδ : 0 < δ) {K c₂ : ℝ} (hK : 1 ≤ K) (hc₂ : 0 < c₂) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x y ψκ : ℝ), 0 < x → x ≤ 1 → 0 < y → y ≤ 1 → ψκ ≤ K * y ^ (-γ) → 1 / (4096 * c₂ * K) * x ^ (-(2 * δ)) ≤ x ^ (1 + γ / 2) / c₂ * y⁻¹ / 4096 → (1 + ψκ) * (((x ^ (1 + γ / 2)) ^ 2)⁻¹ * Real.exp (-(x ^ (1 + γ / 2) / c₂) * y⁻¹ / 4096)) ≤ M * x ^ δ

theorem AVenhance.Infra.Section5.Contracts.n3_arith_final {x y κ ν ψ B A K Cd c₀ c₁ c₂ M₁ M₂ ρ d E D₀ D₁ D₂ R : ℝ} (hK : 1 ≤ K) (hκ : 0 < κ) (hν : 0 < ν) (hνK : ν ≤ K) (hψ : 0 ≤ ψ) (hψκ : ψ ^ 2 ≤ K * κ * ν) (hx : 0 < x) (hρ : 0 < ρ) (hρx : ρ ≤ x) (hd : 0 ≤ d) (hB : 0 ≤ B) (_hA : 0 ≤ A) (hCd : 0 ≤ Cd) (hc₀ : 0 ≤ c₀) (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hM₁ : 0 ≤ M₁) (_hM₂ : 0 ≤ M₂) (hy : 0 ≤ y) (hR : 0 ≤ R) (hE : 0 ≤ E) (hD₀ : 0 ≤ D₀) (hD₁ : 0 ≤ D₁) (hD₂ : 0 ≤ D₂) (hD₀b : √ν * D₀ ≤ A * B) (hD₁b : √ν * D₁ ≤ A * (A / ρ) * B) (hD₂b : √ν * D₂ ≤ A * (A / ρ) * B) (hΛ₁ : y * (1 + R) ≤ M₁ * (ρ * d)) (hΛ₂ : (1 + R) * ((ρ ^ 2)⁻¹ * E) ≤ M₂ * d) : 2 * (144 * Cd * y * (4 * ψ * (1 + R)) * (c₀ * x⁻¹) * D₀ + 144 * Cd * y * (4 * ψ * (1 + R)) * c₁ * D₁ + 144 * Cd * y * (4 * ψ * (1 + R)) * c₁ * D₂ + 144 * Cd * (c₂ * B * (ρ ^ 2)⁻¹) * (4 * ψ * (1 + R)) * E) ≤ 1152 * Cd * (c₀ * M₁ * √K * A + 2 * c₁ * M₁ * √K * A ^ 2 + c₂ * M₂ * K) * d * √κ * B

Assembly of the four terms of the time-integrated centered bound of normie3. With G = 4ψ(1 + ψ/κ), the coefficients 144 C_d y G (c₀ x⁻¹), 144 C_d y G c₁ (twice) and the exponential remainder 144 C_d (c₂ B ρ⁻²) G E give C ε^δ √κ B.