Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324PaperWeightedMajorantNumerics

Common numerical exit from the paper's inserted majorant #

Both parts of paper Step 4 end, after every signed primitive removal, with one integrated primitiveInsertedMajorant. The analytic factor in front is different (endpoint decay alone in Step 4(A), endpoint times central decay in Step 4(B)), but the conversion from the full |lambda_epsilon|^(2m) weight to K^m |log epsilon|^(m-1) is identical.

This file records that scalar conversion once. It contains no physical integral, pairing sum, selector, or triangle inequality.

theorem Anderson4D.exists_r324PaperWeightedMajorantBase {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) :
∃ (K : ℝ), 0 < K ∧ ∀ {epsilon : ℝ} (m : ℕ) (decay value : ℝ), 0 < epsilon → epsilon ≤ 1 / 4 → 1 ≤ |Real.log epsilon| → 2 ≤ m → 0 ≤ decay → |lamEps 1 epsilon| ^ (2 * m) * value ≤ decay * (epsilon⁻¹ ^ 8 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant 1 epsilon supportConstant m z ∂paperMeasure) → value ≤ decay * (↑m ^ 8 * K ^ m * |Real.log epsilon| ^ (m - 1) * epsilon⁻¹ ^ 8)

A paper-weighted estimate by one inserted primitive majorant converts to the standard capped-order ledger. decay is an arbitrary nonnegative factor, so the same theorem applies before or after the central-frequency payoff has been extracted.