The interior-core reduction of the R-324 middle estimate (INEQ 1)

This file quantifies the right-hand side of the mode-free interior estimate R324InteriorCoreMajorantBound and reduces the estimate to a single logarithmic-scale budget on the interior L¹ mass which is free of the coupling λ, the support constant, and the majorant integral:

• le_integral_primitiveInsertedMajorant — the integrated inserted Proposition 4.1 majorant is bounded below by (Cλ)^{2n} · min(c,1)⁴/(c² |log ε|), coming from the near-field term ε⁻²/|log ε| · |z|⁻² 1_{|z| ≤ cε} alone: on the ball |z| ≤ r, r = min (cε) 1, the kernel is at least (cε)⁻² and the ball has paperMeasure at least r⁴;

• R324InteriorCoreLogBudget — the residual scalar inequality 16 |log ε| · (interior L¹ mass) ≤ C^{2m} |log ε|^m;

• r324InteriorCoreMajorantBound_of_logBudget — the budget implies R324InteriorCoreMajorantBound for every coupling λ ≥ 0, because |λ_ε|^{2m} = λ^{2m}/|log ε|^m matches the coupling power of the inserted majorant exactly.

Explicit paperMeasure mass of small boxes

theorem Anderson4D.box_subset_torusDistSq_le (r : ℝ) : (Set.univ.pi fun (x : Fin dim) => Metric.closedBall 0 (r / 2)) ⊆ {z : T4 | torusDistSq z ≤ r ^ 2}

The closed per-coordinate box of radius r/2 lies in the closed torusDistSq-ball of radius r.

theorem Anderson4D.two_pi_mul_haarAddCircle_closedBall (r : ℝ) (hr1 : r ≤ 1) : ENNReal.ofReal (2 * Real.pi) * AddCircle.haarAddCircle (Metric.closedBall 0 (r / 2)) = ENNReal.ofReal r

One coordinate factor: the probability Haar mass of the closed arc of radius r/2 is r/(2π) (as long as r ≤ 2π), stated multiplicatively.

theorem Anderson4D.paperMeasure_box (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : paperMeasure (Set.univ.pi fun (x : Fin dim) => Metric.closedBall 0 (r / 2)) = ENNReal.ofReal (r ^ 4)

The box of per-coordinate radius r/2 has paperMeasure exactly r⁴, for 0 ≤ r ≤ 1.

Lower bound for the integrated inserted majorant

theorem Anderson4D.primitiveInsertedMajorant_nonneg' (C lam ε supportConstant : ℝ) (n : ℕ) (z : T4) : 0 ≤ primitiveInsertedMajorant C lam ε supportConstant n z

The inserted majorant is nonnegative with no sign hypotheses on the coupling: the common exponent 2n is even.

theorem Anderson4D.le_integral_primitiveInsertedMajorant (C lam ε supportConstant : ℝ) (n : ℕ) (hε : 0 < ε) (hε1 : ε ≤ 1) (hsupport : 0 < supportConstant) : (C * lam) ^ (2 * n) * (min supportConstant 1 ^ 4 / (supportConstant ^ 2 * |Real.log ε|)) ≤ ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant n z ∂paperMeasure

Quantitative lower bound for the integrated inserted majorant. The near-field term alone contributes (Cλ)^{2n} · min(c,1)⁴/(c²|log ε|), where c is the support constant: on the punctured box of radius min (cε) 1 the kernel factor is at least (cε)⁻² and the box has paperMeasure mass min (cε) 1 ^ 4.

The residual logarithmic budget

theorem Anderson4D.abs_lamEps_pow_two_mul {lam : ℝ} (hlam : 0 ≤ lam) (ε : ℝ) (m : ℕ) : |lamEps lam ε| ^ (2 * m) = lam ^ (2 * m) / |Real.log ε| ^ m

The doubled coupling power factors through the logarithmic window: |λ_ε|^{2m} = λ^{2m}/|log ε|^m.

def Anderson4D.R324InteriorCoreLogBudget (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (primitiveConstant : ℝ) : Prop

The residual interior-core budget (INEQ 1, reduced form). A single scalar inequality at the logarithmic scale: the interior L¹ mass of every refined fibre, once weighted by one power of |log ε|, is controlled by C^{2m} |log ε|^m. This is the iterated Proposition 4.1 content of the middle estimate; it mentions no coupling λ, no Fourier mode, no majorant integral, and no support constant.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.r324InteriorCoreMajorantBound_of_logBudget {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hlam : 0 ≤ lam) (hsupport : 0 < supportConstant) (budget : R324InteriorCoreLogBudget ρ ε m (min supportConstant 1 ^ 2 / supportConstant * primitiveConstant)) : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant

The logarithmic budget discharges the mode-free interior estimate. The coupling powers match exactly: |λ_ε|^{2m} = λ^{2m}/|log ε|^m on the left, (Cλ)^{2m} inside the integrated majorant on the right; the leftover |log ε|^{m-1} of the budget is absorbed by the 1/|log ε| of the majorant's near-field mass. The support-constant distortion min(c,1)²/c ≤ 1 is paid inside the budget's constant.