Scaling ledger for the endpoint-preserving R-51 estimate

This file converts the natural dyadic logarithm and the compatible periodic mesh in PrimitiveEndpointPeriodic to the real logarithm and covariance scale occurring in Proposition 4.1.

def Anderson4D.primitiveDyadicPeriodLog (q : ℕ) : ℕ

The dyadic logarithm occurring in the endpoint Hepp-tree estimate.

Equations

• Anderson4D.primitiveDyadicPeriodLog q = Nat.log 2 (4 * (2 * q)) + 1

theorem Anderson4D.primitiveDyadicPeriodLog_pos (q : ℕ) : 0 < primitiveDyadicPeriodLog q

theorem Anderson4D.inv_le_eight_mul_compatiblePeriod {ε : ℝ} (hε : 0 < ε) {q : ℕ} (hqε : ↑q = compatibleCellCount ε) : ε⁻¹ ≤ ↑(4 * (2 * q))

The reciprocal covariance scale is below the compatible period count, and hence below the enlarged dyadic carrier used by R-51.

theorem Anderson4D.abs_log_le_primitiveDyadicPeriodLog {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {q : ℕ} (hqε : ↑q = compatibleCellCount ε) : |Real.log ε| ≤ ↑(primitiveDyadicPeriodLog q)

The real logarithmic scale is bounded above by the natural dyadic logarithm selected by the compatible period.

theorem Anderson4D.primitiveDyadicPeriodLog_le_hundred_abs_log {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hlogLarge : 2 ≤ |Real.log ε|) {q : ℕ} (hqε : ↑q = compatibleCellCount ε) : ↑(primitiveDyadicPeriodLog q) ≤ 100 * |Real.log ε|

A coarse upper comparison in the small-scale regime used below.

The deliberately generous factor 100 absorbs the harmless ceiling and torus-period constants already when 2 ≤ |log ε|. This weaker threshold is essential at the public Proposition 4.1 boundary: together with 2 ≤ n and n ≤ |log ε|, it covers every order up to the paper's truncation ⌊|log ε|⌋.

theorem Anderson4D.order_le_primitiveDyadicPeriodLog {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {n q : ℕ} (_hn : 1 ≤ n) (horder : ↑n ≤ |Real.log ε|) (hqε : ↑q = compatibleCellCount ε) : n ≤ primitiveDyadicPeriodLog q

Up to the paper's full truncation window n ≤ |log ε|, the R-51 hypothesis is available with the fixed natural constant K = 1.

Exponential absorption of the Hepp-tree coefficient

theorem Anderson4D.real_natCast_sq_le_four_pow (n : ℕ) (hn : 2 ≤ n) : ↑n ^ 2 ≤ 4 ^ n

theorem Anderson4D.two_le_two_pow (n : ℕ) (hn : 1 ≤ n) : 2 ≤ 2 ^ n

noncomputable def Anderson4D.primitiveEndpointCoefficientBase (C : ℝ) : ℝ

A single fixed base which absorbs every non-logarithmic factor in primitiveEndpointUniformCoefficient C M n 1.

Equations

• Anderson4D.primitiveEndpointCoefficientBase C = 4 ^ 8 * (2 * (16 + (16 * Anderson4D.volumeEstimateFinalConstant) ^ 2 * (2 * (8192 * C))))

theorem Anderson4D.primitiveEndpointCoefficientBase_pos {C : ℝ} (hC : 0 ≤ C) : 0 < primitiveEndpointCoefficientBase C

theorem Anderson4D.primitiveEndpointUniformCoefficient_le_base_pow {C : ℝ} (hC : 0 ≤ C) (M n : ℕ) (hn : 2 ≤ n) : primitiveEndpointUniformCoefficient C M n 1 ≤ primitiveEndpointCoefficientBase C ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)

The full endpoint coefficient is one exponential times the exact L^(n-2) critical logarithmic power.

Simplifying the periodic endpoint bound

def Anderson4D.primitiveR51EndpointConstant (R : ℝ) : ℝ

Equations

• Anderson4D.primitiveR51EndpointConstant R = (160000 * (R + 2) ^ 4) ^ 2 * (9 * (1 + 4 * R ^ 2)) ^ 2

theorem Anderson4D.primitiveR51EndpointConstant_nonneg (R : ℝ) : 0 ≤ primitiveR51EndpointConstant R

noncomputable def Anderson4D.primitiveR51ExponentialBase (C R : ℝ) : ℝ

Fixed exponential base for the purely discrete and endpoint-geometric part of R-51.

Equations

• Anderson4D.primitiveR51ExponentialBase C R = Real.exp 24 * 3 ^ 8 * 4 * Anderson4D.primitiveEndpointCoefficientBase C * (1 + Anderson4D.primitiveR51EndpointConstant R)

theorem Anderson4D.primitiveR51ExponentialBase_pos {C R : ℝ} (hC : 0 ≤ C) : 0 < primitiveR51ExponentialBase C R

theorem Anderson4D.primitiveR51GlobalDecayBound_le_exponential {C : ℝ} (hC : 0 ≤ C) {n q : ℕ} (hn : 2 ≤ n) (δ R : ℝ) (z w : T4) : primitiveR51GlobalDecayBound C n q 1 δ R z w ≤ primitiveR51ExponentialBase C R ^ n * ↑(primitiveDyadicPeriodLog q) ^ (n - 2) * δ ^ 4 * (torusDistSq (z - w) + δ ^ 2)⁻¹ ^ 2

R-51 after all fixed combinatorial factors have been absorbed into one exponential. The only order-dependent remainder is the critical L^(n-2) factor.

Compatible-mesh cancellations

theorem Anderson4D.compatibleMesh_invFour_cancel {ε : ℝ} (hε : 0 < ε) (n : ℕ) : (ε⁻¹ ^ 4) ^ n * compatibleMeshSize ε ^ (4 * n) ≤ 1

theorem Anderson4D.compatibleMesh_invEndpointSq_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (z w : T4) : (torusDistSq (z - w) + compatibleMeshSize ε ^ 2)⁻¹ ^ 2 ≤ 16 * (torusDistSq (z - w) + ε ^ 2)⁻¹ ^ 2

Replacing the compatible mesh by the covariance scale costs at most 16 in the inserted endpoint decay.

theorem Anderson4D.compatibleMesh_invEndpointCube_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (z w : T4) : (torusDistSq (z - w) + ε ^ 2)⁻¹ * (torusDistSq (z - w) + compatibleMeshSize ε ^ 2)⁻¹ ^ 2 ≤ 16 * (torusDistSq (z - w) + ε ^ 2)⁻¹ ^ 3

The same comparison with one additional endpoint factor, as needed for the ordinary (non-inserted) kernel.

Covariance and cell-volume power ledger

theorem Anderson4D.fixed_mul_pow_sub_le_pow {c a : ℝ} (hc : 0 ≤ c) (ha : 0 ≤ a) (m n k : ℕ) (hn : 1 ≤ n) : c * a ^ (m * n - k) ≤ ((1 + c) * (1 + a) ^ m) ^ n

A fixed nonnegative multiplier and a power with a bounded exponent deficit are absorbed into one exponential base.

noncomputable def Anderson4D.primitiveR51FarCore (R : ℝ) : ℝ

Equations

• Anderson4D.primitiveR51FarCore R = (12 + 32 * R ^ 2) * Anderson4D.terminalRadiusFactor R

def Anderson4D.primitiveR51FarStep (Ccell R : ℝ) : ℝ

Equations

• Anderson4D.primitiveR51FarStep Ccell R = Ccell * (R ^ 2 + R ^ 4)

def Anderson4D.primitiveR51NearStep (Ccell R : ℝ) : ℝ

Equations

• Anderson4D.primitiveR51NearStep Ccell R = Ccell * Anderson4D.cellChainRadiusFactor R

noncomputable def Anderson4D.primitiveR51CellCoreBase (Ccell R : ℝ) : ℝ

Exponential base absorbing both cellwise analytic branches.

Equations

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

theorem Anderson4D.primitiveR51CellCoreBase_pos {Ccell R : ℝ} (hCcell : 0 < Ccell) (hR : 0 < R) : 0 < primitiveR51CellCoreBase Ccell R

theorem Anderson4D.primitiveR51CellCoefficients_le {Ccell R δ : ℝ} (hCcell : 0 < Ccell) (hR : 0 < R) (n : ℕ) (hn : 2 ≤ n) : have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); farCoeff + nearCoeff ≤ primitiveR51CellCoreBase Ccell R ^ n * δ ^ (4 * n - 4)

Both branches of the cellwise R-51 estimate share the exact δ^(4n-4) factor and have a uniform exponential coefficient.

noncomputable def Anderson4D.primitiveR51AnalyticBase (Ccov Ccell R : ℝ) : ℝ

Covariance scaling and cell volume cancel exactly at the compatible mesh, leaving only one fixed exponential.

Equations

• Anderson4D.primitiveR51AnalyticBase Ccov Ccell R = Ccov * Anderson4D.primitiveR51CellCoreBase Ccell R

theorem Anderson4D.primitiveR51AnalyticBase_pos {Ccov Ccell R : ℝ} (hCcov : 0 < Ccov) (hCcell : 0 < Ccell) (hR : 0 < R) : 0 < primitiveR51AnalyticBase Ccov Ccell R

theorem Anderson4D.primitiveR51AnalyticLedger_le {Ccov Ccell : ℝ} (hCcov : 0 < Ccov) (hCcell : 0 < Ccell) {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) (n : ℕ) (hn : 2 ≤ n) : have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; Q * (farCoeff + nearCoeff) * δ ^ 4 ≤ primitiveR51AnalyticBase Ccov Ccell R ^ n

Coupling and logarithmic power cancellation

theorem Anderson4D.lamEps_mul_primitiveDyadicPeriodLog_pow_le {lam ε : ℝ} (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlogLarge : 2 ≤ |Real.log ε|) {q : ℕ} (hqε : ↑q = compatibleCellCount ε) (n : ℕ) (hn : 2 ≤ n) : lamEps lam ε ^ (2 * n) * ↑(primitiveDyadicPeriodLog q) ^ (n - 2) ≤ (100 * lam) ^ (2 * n) / |Real.log ε| ^ 2

The n coupling factors cancel all but two powers of the logarithm after the critical R-51 factor L^(n-2) is inserted. The fixed factor 100 absorbs the comparison between the natural dyadic logarithm and |log ε| throughout the full paper truncation window.

Final exponential base

noncomputable def Anderson4D.primitiveR51TotalBase (C Ccov Ccell R : ℝ) : ℝ

One fixed base absorbing the analytic, combinatorial, and endpoint comparison constants in the higher-order branch of Proposition 4.1.

Equations

• Anderson4D.primitiveR51TotalBase C Ccov Ccell R = 200 * (1 + Anderson4D.primitiveR51AnalyticBase Ccov Ccell R) * (1 + Anderson4D.primitiveR51ExponentialBase C R)

theorem Anderson4D.primitiveR51TotalBase_pos {C Ccov Ccell R : ℝ} (hC : 0 ≤ C) (hCcov : 0 < Ccov) (hCcell : 0 < Ccell) (hR : 0 < R) : 0 < primitiveR51TotalBase C Ccov Ccell R

theorem Anderson4D.primitiveR51FixedFactors_le_totalBase {C Ccov Ccell R lam : ℝ} (hC : 0 ≤ C) (hCcov : 0 < Ccov) (hCcell : 0 < Ccell) (hR : 0 < R) (hlam : 0 < lam) (n : ℕ) (hn : 2 ≤ n) : 16 * (100 * lam) ^ (2 * n) * primitiveR51AnalyticBase Ccov Ccell R ^ n * primitiveR51ExponentialBase C R ^ n ≤ (primitiveR51TotalBase C Ccov Ccell R * lam) ^ (2 * n)

The factor 16 in the compatible-mesh endpoint comparison and the two fixed exponential bases are all absorbed into primitiveR51TotalBase^(2n).

theorem Anderson4D.primitiveR51ScaledAnalyticDecay_le {C Ccov Ccell : ℝ} (hC : 0 ≤ C) (hCcov : 0 < Ccov) (hCcell : 0 < Ccell) {lam ε R : ℝ} (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hR : 0 < R) (hlogLarge : 2 ≤ |Real.log ε|) {q : ℕ} (hqε : ↑q = compatibleCellCount ε) (n : ℕ) (hn : 2 ≤ n) (z w : T4) : have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; lamEps lam ε ^ (2 * n) * (Q * (farCoeff + nearCoeff) * primitiveR51GlobalDecayBound C n q 1 δ R z w) ≤ (primitiveR51TotalBase C Ccov Ccell R * lam) ^ (2 * n) * (1 / |Real.log ε| ^ 2) * (torusDistSq (z - w) + ε ^ 2)⁻¹ ^ 2

Complete real-valued scaling ledger for the endpoint-preserving R-51 bound. This is the point where the cell scale, covariance scale, critical dyadic logarithm, coupling, and endpoint comparison are all simultaneously discharged.