recombine the low Fourier trace and analytic tail

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceRecombination.orderedRealDerivative_contDiff_instance (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (orderedRealDerivative w f)

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceRecombination.orderedRealDerivative_add_instance (w : List (Fin 2)) {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : orderedRealDerivative w (f + g) = orderedRealDerivative w f + orderedRealDerivative w g

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceRecombination.continuous_cell_l2_add_le {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (f x + g x) ^ 2) ≤ √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x ^ 2) + √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x ^ 2)

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceRecombination.ordered_eq_classical_instance (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : orderedRealDerivative w f = Section4.classicalWordDerivative w f

theorem AVenhance.Infra.Section5.RelativeError.e44_initialDerivative_cell_l2_le_low_add_high {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (M : ℕ) (w : List (Fin 2)) : √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w g x ^ 2) ≤ √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w (Ergodic.lowProjection g M) x ^ 2) + √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w (Ergodic.highRemainder g M) x ^ 2)

A positive-order derivative of the sum of the low projection and its spectral complement is bounded by the sum of their cell L² bounds.

theorem AVenhance.Infra.Section5.RelativeError.e44_initialDerivative_bound_of_low_high {w : List (Fin 2)} {r R A ν S N Cₚ Cₜ c low high total : ℝ} (hr : 0 < r) (hR : r ≤ R) (hA : 1 ≤ A) (hν : 0 < ν) (hS : 0 ≤ S) (hN : 0 ≤ N) (hCp : 0 ≤ Cₚ) (hCt : 1 ≤ Cₜ) (habs : (√ν)⁻¹ * Real.exp (-c * R * (A / r)) ≤ 1) (hPoincare : N ≤ Cₚ * (√ν)⁻¹ * S) (hlow : low ≤ 2 * Real.exp 1 * (A / r) ^ w.length * S) (hhigh : high ≤ Cₜ * ↑w.length.factorial * (Cₜ / R) ^ w.length * Real.exp (-c * R * (A / r)) * N) (htotal : total ≤ low + high) : total ≤ (2 * Real.exp 1 + Cₜ * Cₚ) * ↑w.length.factorial * (max A Cₜ / r) ^ w.length * S

The AV-facing scalar assembly used after the low-mode trace and analytic tail estimates have been instantiated. The tail absorption and mean-zero Poincare estimate are kept explicit so callers can verify their exact scales.

noncomputable def AVenhance.Infra.Section5.RelativeError.e44TraceCombinationConstant (A Cₚ Cₜ : ℝ) : ℝ

Explicit scalar used to turn the low/high estimate into a radius-loss trace. It depends only on the cutoff amplitude and the two scalar estimate constants, so it can be fixed before the Ingredients instance.

Equations

• AVenhance.Infra.Section5.RelativeError.e44TraceCombinationConstant A Cₚ Cₜ = max 1 (max (2 * Real.exp 1 + Cₜ * Cₚ) (max A Cₜ))

theorem AVenhance.Infra.Section5.RelativeError.e44_initialTrace_of_spectral_piece_bounds {g : Homogenization.Vec 2 → ℝ} {r R A ν S N Cₚ Cₜ c : ℝ} (M : ℕ) (hg : ContDiff ℝ (↑⊤) g) (hr : 0 < r) (hR : r ≤ R) (hA : 1 ≤ A) (hν : 0 < ν) (hS : 0 ≤ S) (hN : 0 ≤ N) (hCp : 0 ≤ Cₚ) (hCt : 1 ≤ Cₜ) (habs : (√ν)⁻¹ * Real.exp (-c * R * (A / r)) ≤ 1) (hPoincare : N ≤ Cₚ * (√ν)⁻¹ * S) (hLow : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w (Ergodic.lowProjection g M) x ^ 2) ≤ 2 * Real.exp 1 * (A / r) ^ w.length * S) (hHigh : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w (Ergodic.highRemainder g M) x ^ 2) ≤ Cₜ * ↑w.length.factorial * (Cₜ / R) ^ w.length * Real.exp (-c * R * (A / r)) * N) (w : List (Fin 2)) : 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, Section4.classicalWordDerivative w g x ^ 2) ≤ S * (↑w.length.factorial / (r / e44TraceCombinationConstant A Cₚ Cₜ ^ 2) ^ w.length)

Convert the low/high derivative bounds into the exact positive-order initial-trace shape consumed by the theta profile. The reduced radius is r / Ctr^2 and the amplitude remains S.