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.