Final deterministic estimate ledgers

This file closes the numerical end of the deterministic reductions in Deng--Shen, Sections 4.1--4.2. It deliberately separates the two logically different parts of R-322:

• RenormReductionOutput is the off-diagonal pointwise output (4.15) supplied by the interval reduction from Proposition 4.1;
• the theorems below integrate that output, justify every exchange of a finite sum and an integral, and absorb the remaining universal multiplier into the exponential constant. Their conclusion has exactly the ε⁻² |log ε|⁻¹ (C λ)^(2q) shape of (3.22).

Thus no hypothesis merely restates (3.22).

The exact off-diagonal pointwise output of R-322

noncomputable def Anderson4D.endpointFiberDetJSum (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (s : Finset (Fin (2 * q)) × Finset (Fin (2 * q))) (z : T4) : ℝ

The output which paper (4.15) supplies after the Dyck-interval reduction.

The first field is the analytic side condition needed to exchange the finite pairing sum and the spatial integral. The second field is the exact grouped form of (4.15): for each endpoint/Dyck signature one first sums over the compatible primitive pairings, then takes the absolute value, and only then sums over signatures. This order is essential because Proposition 4.1 bounds the primitive-pairing sum rather than the sum of its termwise absolute values.

The predicate packages iterative primitive-block removal and the three Taylor/symmetry cases (4.10)--(4.12). The estimate is stated away from z = 0, matching the inverse-square estimate in the paper; that single Haar-null point is discarded only when the bound is integrated below.

Equations

• Anderson4D.endpointFiberDetJSum ρ lam ε q s z = ∑ σ ∈ Anderson4D.nonSplitPairings q with Anderson4D.reductionEndpointSignature σ = s, Anderson4D.detJ ρ lam ε q σ z 0

noncomputable def Anderson4D.groupedDetJAbsSum (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (z : T4) : ℝ

Equations

• Anderson4D.groupedDetJAbsSum ρ lam ε q z = ∑ s ∈ Anderson4D.nonSplitReductionEndpointSignatures q, |Anderson4D.endpointFiberDetJSum ρ lam ε q s z|

def Anderson4D.RenormReductionOutput (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (primitiveConstant supportConstant : ℝ) : Prop

Equations

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

Discharging the endpoint-signature count

def Anderson4D.RenormFiberReductionOutput (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (primitiveConstant supportConstant : ℝ) : Prop

The exact fixed-signature analytic output left after Step 1 of the R-322 reduction. Unlike RenormReductionOutput, the pointwise bound is required separately for each realized endpoint signature.

Equations

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

theorem Anderson4D.RenormFiberReductionOutput.toRenormReductionOutput {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hred : RenormFiberReductionOutput ρ lam ε q primitiveConstant supportConstant) : RenormReductionOutput ρ lam ε q (4 * primitiveConstant) supportConstant

Summing the fixed-signature estimate costs exactly the coarse 4^(2q) factor from Step 1, which is absorbed by replacing the primitive constant C with 4C.

theorem Anderson4D.abs_renormC2q_le_integral_primitiveKernelMajorant {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hred : RenormReductionOutput ρ lam ε q primitiveConstant supportConstant) : |renormC2q ρ lam ε q| ≤ ∫ (z : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant q z ∂paperMeasure

The off-diagonal pointwise R-322 output dominates the exact renormalization constant after integration. The proof preserves the paper's order of operations: regroup by endpoint signature, sum within each fiber, take absolute values, then sum over signatures. All finite-sum/integral interchanges are licensed by the integrability field of RenormReductionOutput; the omitted point z = 0 is Haar-null.

Integration and absorption of universal constants

theorem Anderson4D.exists_abs_renormC2q_le_raw : ∃ (Cball : ℝ) (Creg : ℝ), 0 < Cball ∧ 0 < Creg ∧ ∀ (ρ : SmoothCutoff) (primitiveConstant supportConstant lam ε : ℝ) (q : ℕ), 0 < ε → 0 < supportConstant → 1 ≤ |Real.log ε| → RenormReductionOutput ρ lam ε q primitiveConstant supportConstant → |renormC2q ρ lam ε q| ≤ (primitiveConstant * lam) ^ (2 * q) * ((Cball * supportConstant ^ 2 + Creg) * ε⁻¹ ^ 2 / |Real.log ε|)

Raw integrated form of (4.15). The constants Cball and Creg are chosen once and are independent of the cutoff support radius, scale, coupling, perturbative order, and pointwise primitive constant.

theorem Anderson4D.mul_constant_le_absorbed_even_pow {base K : ℝ} {q : ℕ} (hbase : 0 ≤ base) (hK : 0 ≤ K) (hq : 1 ≤ q) : base ^ (2 * q) * K ≤ (base * (K + 1)) ^ (2 * q)

A nonnegative order-independent multiplier can be absorbed into the base of an even power at every positive perturbative order.

theorem Anderson4D.exists_renormC_bound_of_reduction {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (Crenorm : ℝ), 0 < Crenorm ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ), 0 ≤ lam → 0 < ε → 1 ≤ |Real.log ε| → 1 ≤ q → RenormReductionOutput ρ lam ε q primitiveConstant supportConstant → |renormC2q ρ lam ε q| ≤ ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)

Numerical closure of R-322, paper (3.22).

For a fixed cutoff support constant and primitive-estimate constant, the universal integration constants are absorbed into one positive named constant, chosen before λ, ε, and q. The only remaining premise is the genuinely off-diagonal pointwise reduction output (4.15), which is sufficient because the numerical closure uses it only under an integral.

R-324: exact frequency-decay ledger

def Anderson4D.leftMomentIndex {m : ℕ} (i : Fin m) : Fin (2 * m)

Embed a left-copy internal index into the doubled carrier used by the deterministic Wick pairing sum.

Equations

• Anderson4D.leftMomentIndex i = ⟨↑i, ⋯⟩

def Anderson4D.rightMomentIndex {m : ℕ} (i : Fin m) : Fin (2 * m)

Embed a right-copy internal index into the doubled carrier used by the deterministic Wick pairing sum.

Equations

• Anderson4D.rightMomentIndex i = ⟨m + ↑i, ⋯⟩

noncomputable def Anderson4D.momentCrossCovarianceProduct (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : ℝ

The cross-covariance factors produced by a bijection between the single indices of two partial pairings. Together with the covariance factors already present in the two detIntegrands, this is the full pairing of the doubled carrier described between (4.16) and (4.18).

Equations

• Anderson4D.momentCrossCovarianceProduct ρ ε m κp κm π v = ∏ i : ↥κp.singles, ρ.etaEpsT4 ε (v (Anderson4D.leftMomentIndex ↑i) - v (Anderson4D.rightMomentIndex ↑(π i)))

noncomputable def Anderson4D.deterministicMomentIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

One deterministic integrand in the second moment of the order-m parametrix coefficient.

The four characters combine to exp(i α·(x-z) + i β·(y-w)) as in (4.18). The two closed deterministic profiles contain the within-copy pairing factors; π supplies exactly the cross-copy Wick contractions.

Equations

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

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

Concrete L3 deterministic pairing sum underlying (3.24).

This is the result of the Wick reduction before probability is introduced: sum over the two within-copy partial pairings and over every bijection of their single sets, followed by the physical integral (4.18). If the single sets have different cardinalities the Equiv sum is empty, as required. The global λ_ε^(2m) is kept exactly once outside the profiles.

The Wick reduction identifies the second moment of pmCoeff with this quantity. R-324 is the purely deterministic task of bounding its norm.

Equations

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

def Anderson4D.z4FrequencyNorm (k : Z4) : ℝ

Euclidean size of a Fourier mode in ℤ⁴.

Equations

• Anderson4D.z4FrequencyNorm k = ‖fun (i : Fin Anderson4D.dim) => ↑(k i)‖

theorem Anderson4D.z4FrequencyNorm_nonneg (k : Z4) : 0 ≤ z4FrequencyNorm k

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

The endpoint multiplier ⟨k⟩⁻⁴ from (3.24), in a form avoiding fractional real powers.

Equations

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

theorem Anderson4D.fourthOrderModeDecay_nonneg (k : Z4) : 0 ≤ fourthOrderModeDecay k

theorem Anderson4D.fourthOrderModeDecay_le_one (k : Z4) : fourthOrderModeDecay k ≤ 1

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

The complete decay branch printed in (3.24): ε⁻⁸ ⟨α⟩⁻⁴ ⟨β⟩⁻⁴ ⟨ε²(α+β)⟩⁻⁸.

Equations

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

theorem Anderson4D.deterministicMomentDecay_nonneg (ε : ℝ) (α β : Z4) : 0 ≤ deterministicMomentDecay ε α β

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

Exact deterministic right side underlying (3.24). outerConstant is the paper's leading absolute C, while powerConstant is the constant inside (Cλ)^(2m-2); keeping them distinct follows DESIGN §5.4's named constant policy.

Equations

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

theorem Anderson4D.deterministicMomentRHS_nonneg {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : 0 ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β

theorem Anderson4D.exists_increment_with_eighth_order_payoff {E : Type u_1} [SeminormedAddCommGroup E] (N : ℕ) (hN : 0 < N) (δ : Fin N → E) (ε : ℝ) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hNtrunc : N ≤ truncOrder ε) : ∃ (i : Fin N), eighthOrderFrequencyDecay ‖δ i‖ ≤ eighthOrderFrequencyDecay (ε ^ 2 * ‖∑ j : Fin N, δ j‖)

The frequency-routing statement at the actual truncation length, already converted to the exact eighth-order payoff in (3.24).

theorem Anderson4D.exists_increment_with_full_moment_decay {E : Type u_1} [SeminormedAddCommGroup E] (N : ℕ) (hN : 0 < N) (δ : Fin N → E) (ε : ℝ) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hNtrunc : N ≤ truncOrder ε) (α β : Z4) (htotal : ‖∑ j : Fin N, δ j‖ = z4FrequencyNorm (α + β)) : ∃ (i : Fin N), ε⁻¹ ^ 8 * fourthOrderModeDecay α * fourthOrderModeDecay β * eighthOrderFrequencyDecay ‖δ i‖ ≤ deterministicMomentDecay ε α β

Frequency routing remains valid after multiplying by the two endpoint decays and the explicit ε⁻⁸ loss. The equality premise is the algebraic composition identity identifying the telescoping shift with α+β.

Combining the two R-324 branches

theorem Anderson4D.le_mul_min_of_le_of_le_mul {value amplitude decay : ℝ} (huniform : value ≤ amplitude) (hdecay : value ≤ amplitude * decay) : value ≤ amplitude * min 1 decay

A uniform estimate and a frequency-decaying estimate combine to a single min estimate. This elementary but essential ledger prevents the two separately proved branches of paper §4.2 from being accidentally added (which would lose the stated decay).

theorem Anderson4D.deterministicMoment_bound_of_two_branches {value outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (huniform : value ≤ lamEps lam ε ^ 2 * outerConstant * (powerConstant * lam) ^ (2 * m - 2)) (hdecay : value ≤ lamEps lam ε ^ 2 * outerConstant * (powerConstant * lam) ^ (2 * m - 2) * deterministicMomentDecay ε α β) : value ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β

Numerical closure of the two deterministic branches in R-324.

The premises are the outputs of Steps 1--3 (uniform branch) and Step 4 (frequency branch) for the same concrete deterministic pairing sum. The conclusion is exactly the P-3.5b-det right side, including λ_ε² C(Cλ)^(2m-2) and the minimum with the three decay factors.

This theorem quantifies over the value of the concrete sum so that the numerical combination of the uniform and decay branches is independent of its realization.

theorem Anderson4D.deterministicMomentPairingSum_bound_of_two_branches {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (huniform : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (powerConstant * lam) ^ (2 * m - 2)) (hdecay : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (powerConstant * lam) ^ (2 * m - 2) * deterministicMomentDecay ε α β) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β

Concrete specialization of the two-branch ledger to the deterministic pairing sum (4.18), combining its uniform and routed R-324 estimates.