Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324PaperResidualEndpointPatternProducer

Paper Step 4(A): the residual endpoint-pattern producer #

This file is the final assembly of the literal four-endpoint argument in paper §4.2. The two signed half transforms are completed before a norm is taken. Their common nested endpoint density is then passed, unchanged, through the existing grouped majorant, complete nested run, and weighted exit.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_r324PaperResidualEndpointPatternWeightedMajorantBound (rho : SmoothCutoff) :
∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ R324PaperResidualEndpointPatternWeightedMajorantBound rho primitiveConstant supportConstant

Uniform paper Step 4(A) producer for the actual endpoint pattern of the refined-fibre representative.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_r324PaperResidualEndpointWeightedMajorantBound (rho : SmoothCutoff) :
∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ R324PaperResidualEndpointWeightedMajorantBound rho primitiveConstant supportConstant

The public residual Step 4(A) input, obtained only after enlarging the literal four-endpoint case product to the paper's uniform eps ^ (-8) budget.