The interior-core logarithmic budget at the base order (m = 1)

The proved keyed L¹ interface provably cannot reach the ε-uniform interior-core budget: at m = 1 its marked slot series is bounded below by ∑ ⟨k⟩⁸‖ρ̂(εk)‖² ≍ ε⁻¹². This file establishes the budget at the base order m = 1 through the physical route instead: the interior Green skeleton of a one-vertex copy is the empty product, so the whole interior L¹ mass is the covariance mass ∫∫ η_ε(v₀−v₁) ≤ (2π)⁸, which is ε-uniform because the periodized covariance has total mass ‖ρ̂(0)‖² ≤ 1 at every scale.

• integral_etaEpsT4_paper_le_one — the total covariance mass, read off the absolutely convergent Fourier series: only the zero mode survives integration, and its coefficient is ⟨2π⟩⁻⁴‖ρ̂(0)‖²·(2π)⁴.
• r324InteriorCoreLogBudget_base — R324InteriorCoreLogBudget ρ ε 1 C at the explicit ε-uniform constant C = 4·(2π)⁴.

theorem Anderson4D.paperMeasure_univ : paperMeasure Set.univ = ENNReal.ofReal ((2 * Real.pi) ^ dim)

Total paperMeasure mass of the torus.

theorem Anderson4D.whiteNoiseFourierScale_sq_mul_pow_dim : NoiseModel.whiteNoiseFourierScale ^ 2 * (2 * Real.pi) ^ dim = 1

The Lebesgue/probability-Haar normalization identity whiteNoiseFourierScale² · (2π)⁴ = 1, in real form.

theorem Anderson4D.integral_etaEpsT4_paper_le_one (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∫ (z : T4), ρ.etaEpsT4 ε z ∂paperMeasure ≤ 1

ε-uniform total covariance mass. The periodized mollified covariance integrates to ‖ρ̂(0)‖² ≤ 1 at every scale 0 < ε: in the absolutely convergent covariance Fourier series only the zero mode survives the integration.

The base order m = 1: structure

instance Anderson4D.instSubsingletonPartialPairingFinOfNatNat : Subsingleton (PartialPairing (Fin 1))

instance Anderson4D.instSubsingletonMomentContractionOfNatNat : Subsingleton (MomentContraction 1)

theorem Anderson4D.r324RenormalizedInteriorCore_one (κ : PartialPairing (Fin 1)) (v : Fin 1 → T4) : r324RenormalizedInteriorCore κ v = 1

A one-vertex copy has no interior Green edge: its renormalized interior core is the empty product.

theorem Anderson4D.pairSlot_classification_two (κ : PartialPairing (Fin (2 * 1))) : {i ∈ κ.pairSupport | i < κ i} = ∅ ∨ {i ∈ κ.pairSupport | i < κ i} = {0} ∧ κ 0 = 1

On the doubled carrier of the base order, an involution either has no ordered pair slot or exactly the slot 0 ↦ 1.

theorem Anderson4D.pi_two_paperMeasure_univ : (MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure) Set.univ = ENNReal.ofReal ((2 * Real.pi) ^ dim) ^ 2

Total mass of the doubled configuration space at the base order.

theorem Anderson4D.integral_primitiveCovarianceProduct_base_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (κ : PartialPairing (Fin (2 * 1))) : MeasureTheory.Integrable (fun (v : Fin (2 * 1) → T4) => primitiveCovarianceProduct ρ ε 1 κ v) (MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure) ∧ (∫ (v : Fin (2 * 1) → T4), primitiveCovarianceProduct ρ ε 1 κ v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * 1)) => paperMeasure) ≤ (2 * Real.pi) ^ 8

ε-uniform covariance-pair mass on the doubled base carrier. For every involution of the two-point carrier, the covariance product integrates to at most (2π)⁸: the empty slot set contributes the raw volume (2π)⁸, and the slot 0 ↦ 1 contributes (2π)⁴ times the ε-uniform covariance mass.

theorem Anderson4D.r324InteriorCoreLogBudget_base (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : R324InteriorCoreLogBudget ρ ε 1 (4 * (2 * Real.pi) ^ 4)

The interior-core logarithmic budget at the base order, at an explicit ε-uniform constant. R324InteriorCoreLogBudget ρ ε 1 C holds with C = 4·(2π)⁴: the base-order interior core has no Green edge, so its L¹ mass is a covariance-pair mass, which is ε-uniform. The keyed L¹ interface, by contrast, has a marked-slot series bounded below by ≍ ε⁻¹² at this order.

theorem Anderson4D.exists_deterministicMoment_paper_bound_base_of_veryHighFrequency : ∃ (outerConstant : ℝ) (pC : ℝ), 0 < outerConstant ∧ 0 < pC ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324VeryHighCentralFrequencySignedBound ρ lam ε 1 (lamEps lam ε ^ 2 * outerConstant * (16 * pC * lam) ^ (2 * 1 - 2)) → ‖deterministicMomentPairingSum ρ lam ε 1 α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * pC) lam ε 1 α β

The base-order paper bound from the very-high residue alone. At m = 1 the interior-core budget is discharged unconditionally above, so the frozen paper (3.24) shape at ε-uniform constants follows from only the very-high-frequency signed residue (‖freq(α+β)‖ > truncOrder ε · ε⁻¹).