Entity-level reduction for the deterministic second moment

This file continues paper Section 4.2 after the concrete L3 pairing sum was frozen in FinalBound.lean.

This module contains the original downstream ledgers for two abstract reduction interfaces:

• MomentUniformReductionOutputAt is a pointwise-density interface. Its density variable is an absolute translation coordinate, whereas the majorant in (4.4) is a surviving relative endpoint. The concrete proof therefore uses the integrated scalar interface in R324PrimitiveIterationClosure instead;
• RoutedMomentReductionOutput is a finite decomposition into concrete summands, each carrying the decay of every possible frequency increment.

Neither abstract output proves either branch of (3.24). This file proves the numerical consequences of the stated hypotheses; the final concrete R-324 closure uses the integrated interface.

The critical regularized square integral

noncomputable def Anderson4D.regularizedInvSquare (ε : ℝ) (z : T4) : ℝ

The regularized power in the second term of the inserted primitive majorant (4.4).

Equations

• Anderson4D.regularizedInvSquare ε z = (Anderson4D.torusDistSq z + ε ^ 2)⁻¹ ^ 2

theorem Anderson4D.regularizedInvSquare_nonneg (ε : ℝ) (z : T4) : 0 ≤ regularizedInvSquare ε z

theorem Anderson4D.measurable_regularizedInvSquare (ε : ℝ) : Measurable (regularizedInvSquare ε)

theorem Anderson4D.integrable_regularizedInvSquare (ε : ℝ) (hε : 0 < ε) : MeasureTheory.Integrable (regularizedInvSquare ε) paperMeasure

theorem Anderson4D.regularizedInvSquare_le_inv_four (ε : ℝ) (hε : 0 < ε) (z : T4) : regularizedInvSquare ε z ≤ ε⁻¹ ^ 4

On the inner ball the regularized square is bounded by ε⁻⁴.

theorem Anderson4D.regularizedInvSquare_le_invSqKer_sq (ε : ℝ) (hε : 0 < ε) (z : T4) (hz : ε ^ 2 ≤ torusDistSq z) : regularizedInvSquare ε z ≤ invSqKer z ^ 2

Outside the scale-ε ball the regularized square is bounded by the critical kernel |z|⁻⁴.

def Anderson4D.momentInnerBall (ε : ℝ) : Set T4

Equations

• Anderson4D.momentInnerBall ε = {z : Anderson4D.T4 | Anderson4D.torusDistSq z ≤ ε ^ 2}

def Anderson4D.momentOuterAnnulus (ε : ℝ) : Set T4

Equations

• Anderson4D.momentOuterAnnulus ε = {z : Anderson4D.T4 | ε ^ 2 ≤ Anderson4D.torusDistSq z}

theorem Anderson4D.measurableSet_momentInnerBall (ε : ℝ) : MeasurableSet (momentInnerBall ε)

theorem Anderson4D.measurableSet_momentOuterAnnulus (ε : ℝ) : MeasurableSet (momentOuterAnnulus ε)

theorem Anderson4D.integrableOn_invSqKer_sq_momentOuterAnnulus (ε : ℝ) (hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (z : T4) => invSqKer z ^ 2) (momentOuterAnnulus ε) paperMeasure

theorem Anderson4D.momentInnerBall_subset_metricBall (ε : ℝ) (hε : 0 < ε) : momentInnerBall ε ⊆ Metric.ball 0 (2 * ε)

The scale ball is contained in the metric ball of twice the radius. The harmless factor 2 avoids a closed/open boundary issue.

theorem Anderson4D.integral_regularizedInvSquare_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → ∫ (z : T4), regularizedInvSquare ε z ∂paperMeasure ≤ C * (1 + |Real.log ε|)

The critical regularized square has only a logarithmic integral divergence in four dimensions.

Integrating the inserted Proposition 4.1 majorant

theorem Anderson4D.integrable_primitiveInsertedMajorant (C lam ε supportConstant : ℝ) (n : ℕ) (hε : 0 < ε) : MeasureTheory.Integrable (primitiveInsertedMajorant C lam ε supportConstant n) paperMeasure

theorem Anderson4D.primitiveKernelMajorant_le_invSq_mul_inserted (C lam ε supportConstant : ℝ) (n : ℕ) (z : T4) (hε : 0 < ε) : primitiveKernelMajorant C lam ε supportConstant n z ≤ ε⁻¹ ^ 2 * primitiveInsertedMajorant C lam ε supportConstant n z

Giving up one quadratic diameter insertion costs exactly ε⁻²: the ordinary primitive majorant (4.3) is bounded by ε⁻² times the inserted majorant (4.4). Paper §4.2 Step 4 uses this once at each of the four external endpoints.

theorem Anderson4D.four_endpoint_invSq_loss (ε : ℝ) : (ε⁻¹ ^ 2) ^ 4 = ε⁻¹ ^ 8

Four endpoint sacrifices produce the explicit ε⁻⁸ loss in (3.24).

theorem Anderson4D.exists_integral_primitiveInsertedMajorant_le : ∃ (Cball : ℝ) (Creg : ℝ), 0 < Cball ∧ 0 < Creg ∧ ∀ (C lam ε supportConstant : ℝ) (n : ℕ), 0 < ε → ε ≤ 1 → 0 < supportConstant → 1 ≤ |Real.log ε| → ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant n z ∂paperMeasure ≤ (C * lam) ^ (2 * n) * ((Cball * supportConstant ^ 2 + 2 * Creg) / |Real.log ε|)

The inserted majorant integrates to one inverse logarithm. This is the radial calculation used after the final primitive reduction in paper §4.2 Step 3.

Uniform grouped branch of R-324

noncomputable def Anderson4D.deterministicMomentPairingTerm (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : ℂ

One contraction term in the concrete deterministic moment sum, before the common λ_ε^(2m) factor.

Equations

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

theorem Anderson4D.deterministicMomentPairingSum_eq_nested_terms (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) : deterministicMomentPairingSum ρ lam ε m α β = ↑(lamEps lam ε) ^ (2 * m) * ∑ κp : PartialPairing (Fin m), ∑ κm : PartialPairing (Fin m), ∑ π : ↥κp.singles ≃ ↥κm.singles, deterministicMomentPairingTerm ρ ε m α β κp κm π

The frozen deterministic moment sum is exactly the common coupling times the three finite contraction sums from (4.18).

noncomputable def Anderson4D.deterministicMomentContractionTerm (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (e : MomentContraction m) : ℂ

A contraction term indexed by the single doubled-entity type.

Equations

• Anderson4D.deterministicMomentContractionTerm ρ ε m α β e = Anderson4D.deterministicMomentPairingTerm ρ ε m α β e.fst e.snd.fst e.snd.snd

theorem Anderson4D.deterministicMomentPairingSum_eq_contractionTerms (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) : deterministicMomentPairingSum ρ lam ε m α β = ↑(lamEps lam ε) ^ (2 * m) * ∑ e : MomentContraction m, deterministicMomentContractionTerm ρ ε m α β e

Entity-indexed form of the frozen deterministic moment sum.

noncomputable def Anderson4D.groupedDeterministicMomentTermNormSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) : ℝ

The cancellation-preserving Step 1 quantity for R-324: sum the contraction terms sharing a doubled extraction signature before taking their norm.

Equations

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

theorem Anderson4D.deterministicMomentPairingSum_le_groupedSignatures (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ |lamEps lam ε| ^ (2 * m) * groupedDeterministicMomentTermNormSum ρ ε m α β

Triangle inequality only across doubled endpoint signatures. No absolute value is moved inside a primitive-pairing fiber.

structure Anderson4D.MomentUniformReductionData (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Type

Cancellation-preserving upstream data produced by the successive primitive reductions (4.18)--(4.20).

The density is indexed by the extraction signature of the doubled full pairing. All contraction terms in one signature fiber are summed before their norm is taken, exactly as the primitive-pairing sums in Proposition 4.1 require. The integrability field licenses the final finite sum/integral exchange, and the pointwise field is strictly upstream of the integrated conclusion (3.24).

• density : Finset (Fin (2 * m)) × Finset (Fin (2 * m)) → T4 → ℝ
• density_integrable (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → MeasureTheory.Integrable (self.density s) paperMeasure
• density_nonneg (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ∀ (z : T4), 0 ≤ self.density s z
• fiber_le_density_integral (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ‖∑ e : MomentContraction m with momentContractionSignature e = s, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ ∫ (z : T4), self.density s z ∂paperMeasure
• pointwise_primitive_domination (z : T4) : |lamEps lam ε| ^ (2 * m) * ∑ s ∈ momentContractionSignatures m, self.density s z ≤ primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z

structure Anderson4D.MomentFiberReductionData (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Type

Fixed-signature pointwise-density interface.

The concrete R-324 proof instead uses MomentRefinedIntegratedReductionData: density here is parameterized by an absolute translation coordinate, whereas the paper integrates all external variables before majorizing the surviving relative endpoint.

• density : Finset (Fin (2 * m)) × Finset (Fin (2 * m)) → T4 → ℝ
• density_integrable (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → MeasureTheory.Integrable (self.density s) paperMeasure
• density_nonneg (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ∀ (z : T4), 0 ≤ self.density s z
• fiber_le_density_integral (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ‖∑ e : MomentContraction m with momentContractionSignature e = s, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ ∫ (z : T4), self.density s z ∂paperMeasure
• pointwise_fiber_domination (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ∀ (z : T4), |lamEps lam ε| ^ (2 * m) * self.density s z ≤ primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z

def Anderson4D.MomentFiberReductionData.toMomentUniformReductionData {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (d : MomentFiberReductionData ρ lam ε m α β primitiveConstant supportConstant) : MomentUniformReductionData ρ lam ε m α β (4 * primitiveConstant) supportConstant

Sum the independent fixed-signature collapse estimates and absorb the exact coarse 4^(2m) signature count by replacing C with 4C. This is the R-324 counterpart of RenormFiberReductionOutput.toRenormReductionOutput.

Equations

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

def Anderson4D.MomentUniformReductionOutputAt (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Prop

Equations

• Anderson4D.MomentUniformReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant = Nonempty (Anderson4D.MomentUniformReductionData ρ lam ε m α β primitiveConstant supportConstant)

theorem Anderson4D.MomentFiberReductionData.toMomentUniformReductionOutputAt {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (d : MomentFiberReductionData ρ lam ε m α β primitiveConstant supportConstant) : MomentUniformReductionOutputAt ρ lam ε m α β (4 * primitiveConstant) supportConstant

Existence wrapper for the fixed-signature constructor.

theorem Anderson4D.deterministicMomentPairingSum_le_integral_insertedMajorant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hred : MomentUniformReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure

Integrate the genuine pointwise primitive domination supplied by the uniform reduction.

theorem Anderson4D.exists_deterministicMoment_uniform_bound_of_reduction {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentUniformReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (primitiveConstant * lam) ^ (2 * m - 2)

Uniform entity branch of P-3.5b-det.

For fixed constants coming from Proposition 4.1, the radial integration constants are chosen once and absorbed into the paper's leading absolute constant. The conclusion is the exact uniform branch λ_ε² C (Cλ)^(2m-2).

Routed entity branch of R-324

noncomputable def Anderson4D.secondOrderModeDecay (k : Z4) : ℝ

The endpoint Green multiplier ⟨k⟩⁻².

Equations

• Anderson4D.secondOrderModeDecay k = (1 + Anderson4D.z4FrequencyNorm k ^ 2)⁻¹

theorem Anderson4D.secondOrderModeDecay_nonneg (k : Z4) : 0 ≤ secondOrderModeDecay k

def Anderson4D.paperModeNormSq (k : Z4) : ℝ

The squared Euclidean frequency used by the paper's Japanese bracket.

Equations

• Anderson4D.paperModeNormSq k = ∑ i : Fin Anderson4D.dim, ↑(k i) ^ 2

noncomputable def Anderson4D.paperSecondOrderModeDecay (k : Z4) : ℝ

Equations

• Anderson4D.paperSecondOrderModeDecay k = (1 + Anderson4D.paperModeNormSq k)⁻¹

noncomputable def Anderson4D.paperFourthOrderModeDecay (k : Z4) : ℝ

Equations

• Anderson4D.paperFourthOrderModeDecay k = ((1 + Anderson4D.paperModeNormSq k) ^ 2)⁻¹

theorem Anderson4D.paperSecondOrderModeDecay_nonneg (k : Z4) : 0 ≤ paperSecondOrderModeDecay k

theorem Anderson4D.paperFourthOrderModeDecay_nonneg (k : Z4) : 0 ≤ paperFourthOrderModeDecay k

theorem Anderson4D.z4FrequencyNorm_sq_le_sum (k : Z4) : z4FrequencyNorm k ^ 2 ≤ ∑ i : Fin dim, ↑(k i) ^ 2

Sup-norm comparison for the project's real Fourier vectors.

theorem Anderson4D.norm_paperFourierCoeff_greenFn_eq (k : Z4) : ‖∫ (z : T4), charT4 k z * ↑(greenFn z) ∂paperMeasure‖ = paperSecondOrderModeDecay k

Exact Green coefficient in the paper's Euclidean bracket.

theorem Anderson4D.paperSecondOrderModeDecay_le (k : Z4) : paperSecondOrderModeDecay k ≤ secondOrderModeDecay k

Euclidean bracket decay is at least as strong as the project's sup-norm bracket decay.

theorem Anderson4D.norm_paperFourierCoeff_greenFn_le (k : Z4) : ‖∫ (z : T4), charT4 k z * ↑(greenFn z) ∂paperMeasure‖ ≤ secondOrderModeDecay k

The heat-kernel Green construction supplies the endpoint multiplier used in §4.2 Step 4. The project uses the sup norm on R4, so this is the faithful one-sided comparison with the paper's Euclidean bracket.

theorem Anderson4D.secondOrderModeDecay_sq (k : Z4) : secondOrderModeDecay k ^ 2 = fourthOrderModeDecay k

theorem Anderson4D.paperSecondOrderModeDecay_sq (k : Z4) : paperSecondOrderModeDecay k ^ 2 = paperFourthOrderModeDecay k

theorem Anderson4D.paperFourthOrderModeDecay_le (k : Z4) : paperFourthOrderModeDecay k ≤ fourthOrderModeDecay k

theorem Anderson4D.four_endpoint_green_decay_le (α β : Z4) : ‖∫ (z : T4), charT4 α z * ↑(greenFn z) ∂paperMeasure‖ ^ 2 * ‖∫ (z : T4), charT4 β z * ↑(greenFn z) ∂paperMeasure‖ ^ 2 ≤ fourthOrderModeDecay α * fourthOrderModeDecay β

Two Green endpoints on each copy are bounded by the ⟨α⟩⁻⁴⟨β⟩⁻⁴ factor.

theorem Anderson4D.four_endpoint_green_paper_decay (α β : Z4) : ‖∫ (z : T4), charT4 α z * ↑(greenFn z) ∂paperMeasure‖ ^ 2 * ‖∫ (z : T4), charT4 β z * ↑(greenFn z) ∂paperMeasure‖ ^ 2 = paperFourthOrderModeDecay α * paperFourthOrderModeDecay β

Exact Euclidean-bracket version of the preceding four-endpoint identity.

theorem Anderson4D.endpoint_phase_decay_le_two (k : Z4) (θ : ℝ) : secondOrderModeDecay k * |Real.cos θ - 1| ≤ 2 * secondOrderModeDecay k

Bounded endpoint oscillation preserves one Green Fourier decay while costing the explicit factor 2, as in the last paragraph of §4.2.

theorem Anderson4D.endpoint_phase_decay_le_quadratic (k : Z4) (θ : ℝ) : secondOrderModeDecay k * |Real.cos θ - 1| ≤ secondOrderModeDecay k * θ ^ 2

The alternative quadratic endpoint bound is the diameter insertion used in Steps 1 and 3.

def Anderson4D.z4EuclideanFrequency (k : Z4) : EuclideanSpace ℝ (Fin dim)

Cast a Fourier mode to Euclidean frequency space, so the routing argument produces the paper's exact Japanese bracket rather than merely an equivalent sup-norm bracket.

Equations

• Anderson4D.z4EuclideanFrequency k = WithLp.toLp 2 fun (i : Fin Anderson4D.dim) => ↑(k i)

theorem Anderson4D.norm_sq_z4EuclideanFrequency (k : Z4) : ‖z4EuclideanFrequency k‖ ^ 2 = paperModeNormSq k

noncomputable def Anderson4D.paperDeterministicMomentDecay (ε : ℝ) (α β : Z4) : ℝ

Exact Euclidean decay branch printed in (3.24).

Equations

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

theorem Anderson4D.paperDeterministicMomentDecay_nonneg (ε : ℝ) (α β : Z4) : 0 ≤ paperDeterministicMomentDecay ε α β

theorem Anderson4D.paperDeterministicMomentDecay_le (ε : ℝ) (α β : Z4) : paperDeterministicMomentDecay ε α β ≤ deterministicMomentDecay ε α β

The exact paper decay is stronger than the sup-norm ledger frozen in FinalBound.lean.

structure Anderson4D.RoutedMomentDecomposition (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (amplitude : ℝ) : Type

A finite, term-by-term frequency decomposition of the concrete deterministic moment sum.

This is the entity-level output of paper §4.2 Step 4, before the pigeonhole/routing argument:

• each term is a genuine summand of deterministicMomentPairingSum;
• its increment list telescopes exactly to α+β;
• every possible increment exposes the corresponding cutoff decay;
• the sum of nonnegative term weights is controlled by the already reduced uniform amplitude.

These fields are strictly upstream of the target decay estimate.

• termCount : ℕ
• term : Fin self.termCount → ℂ
• weight : Fin self.termCount → ℝ
• incrementCount : Fin self.termCount → ℕ
• increment (a : Fin self.termCount) : Fin (self.incrementCount a) → EuclideanSpace ℝ (Fin dim)
• sum_eq : deterministicMomentPairingSum ρ lam ε m α β = ∑ a : Fin self.termCount, self.term a
• weight_nonneg (a : Fin self.termCount) : 0 ≤ self.weight a
• incrementCount_pos (a : Fin self.termCount) : 0 < self.incrementCount a
• incrementCount_le_trunc (a : Fin self.termCount) : self.incrementCount a ≤ truncOrder ε
• increment_sum (a : Fin self.termCount) : ∑ i : Fin (self.incrementCount a), self.increment a i = z4EuclideanFrequency (α + β)
• term_le_increment_decay (a : Fin self.termCount) (i : Fin (self.incrementCount a)) : ‖self.term a‖ ≤ self.weight a * (ε⁻¹ ^ 8 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * eighthOrderFrequencyDecay ‖self.increment a i‖)
• sum_weight_le : ∑ a : Fin self.termCount, self.weight a ≤ amplitude

def Anderson4D.RoutedMomentReductionOutput (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (amplitude : ℝ) : Prop

Existence form used as the R-324 reduction interface.

Equations

• Anderson4D.RoutedMomentReductionOutput ρ lam ε m α β amplitude = Nonempty (Anderson4D.RoutedMomentDecomposition ρ lam ε m α β amplitude)

theorem Anderson4D.deterministicMomentPairingSum_paperDecay_bound_of_routedReduction {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} {α β : Z4} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hred : RoutedMomentReductionOutput ρ lam ε m α β amplitude) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ amplitude * paperDeterministicMomentDecay ε α β

The concrete frequency decomposition and the truncation-length routing lemma imply the paper's exact Euclidean decaying branch of (3.24).

theorem Anderson4D.deterministicMomentPairingSum_decay_bound_of_routedReduction {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} {α β : Z4} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hred : RoutedMomentReductionOutput ρ lam ε m α β amplitude) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ amplitude * deterministicMomentDecay ε α β

Compatibility corollary for the sup-norm decay ledger frozen in FinalBound.lean.

Complete conditional closure of P-3.5b-det

noncomputable def Anderson4D.paperDeterministicMomentRHS (outerConstant powerConstant lam ε : ℝ) (m : ℕ) (α β : Z4) : ℝ

Exact Euclidean-bracket right side printed in (3.24).

Equations

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

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_reductions {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentUniformReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → RoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (primitiveConstant * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant primitiveConstant lam ε m α β

Strong, paper-bracket form of the complete deterministic closure.

theorem Anderson4D.exists_deterministicMoment_bound_of_reductions {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentUniformReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → RoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (primitiveConstant * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant primitiveConstant lam ε m α β

Entity-level deterministic second-moment bound, paper (3.24).

The theorem consumes exactly the two strictly upstream outputs modeled above: the final primitive density from Steps 1--3 and the termwise frequency decomposition from Step 4. It returns the exact λ_ε² C(Cλ)^(2m-2) min(1, ...) bound on the frozen concrete L3 pairing sum.