The interior transport at order two: the exact mass and its ε-divergence

This file shows that, beyond the base order, the ε-uniform interior-core budget R324InteriorCoreLogBudget ρ ε m C is false at m = 2 for every cutoff and every constant, and so is the corresponding Statement 1 interface R324InteriorCoreMajorantBound. Thus the endpoint difference factor must be retained at m ≥ 2 to obtain the paper (3.24) scale.

The mechanism. For the two-block schedule (both within-half pairings the full swap) the extraction of each swap block removes the last chain edge and installs the compensating difference factor G(v₁-y) - G(v₀-y) there — but the interior core erases the first and last chain edges into the endpoint legs, which the proved chain then bounds in sup by 16·⟨α⟩⁻⁴⟨β⟩⁻⁴. What stays inside the interior core is the raw middle chain edge G(v₀-v₁) against its own covariance factor η_ε(v₀-v₁) on the same relative coordinate, per half. The parity/Taylor cancellation that renormalizes this block in the true physical integral lives entirely in the discarded endpoint difference factor, so the interior mass is the square of the raw one-block mass:

• integral_greenFn_mul_etaEpsT4_eq — the Green-weighted covariance mass, exactly: ∫ G η_ε = ⟨2π⟩⁻⁴ Σ_k ‖ρ̂(εk)‖² ⟨k⟩⁻²;
• exists_le_integral_greenFn_mul_etaEpsT4 — that mass is ≥ c ε⁻²: all ≈ ε⁻⁴ low modes carry symbol weight ≥ 1/4;
• r324RefinedInteriorCoreIntegral_twoBlock — the two-block interior core equals ((2π)⁴ ∫ G η_ε)² (so it is ≳ ε⁻⁴, against the budget's C^4·|log ε| allowance);
• not_r324InteriorCoreLogBudget_two, not_r324InteriorCoreMajorantBound_two, r324InteriorCoreLogBudget_two_unsatisfiable — the nonexistence theorems.

Difference-retaining formulation. Any true m ≥ 2 interior transport must keep, for every within-half pair (l, m-1) extracted onto the terminal chain edge, that edge's difference factor (or an equivalent ε-gain) inside the interior object; equivalently, the endpoint legs may only be sup-normalized after the terminal blocks are integrated jointly with their difference factors. The base order m = 1 is unaffected: there the interior skeleton is empty (r324InteriorCoreLogBudget_base), and the divergence mechanism needs an adjacent extracted pair, which first exists at m = 2.

The mollifier symbol near frequency zero

theorem Anderson4D.SmoothCutoff.integrable_toFun (ρ : SmoothCutoff) : MeasureTheory.Integrable ρ.toFun MeasureTheory.volume

The mollifier is integrable: its integral is one, not junk.

theorem Anderson4D.norm_exp_neg_I_mul_ofReal_sub_one_le (θ : ℝ) : ‖Complex.exp (-Complex.I * ↑θ) - 1‖ ≤ |θ|

The unit character bound ‖e^{-i θ} - 1‖ ≤ |θ| in the form used below.

theorem Anderson4D.SmoothCutoff.norm_fourierR4_sub_one_le (ρ : SmoothCutoff) (ξ : R4) : ‖fourierR4 ρ.toFun ξ - 1‖ ≤ ρ.radius * ∑ i : Fin dim, |ξ i|

Quantitative continuity of the mollifier symbol at frequency zero: ‖ρ̂(ξ) - 1‖ ≤ radius · Σᵢ |ξᵢ|.

theorem Anderson4D.SmoothCutoff.norm_symbol_sub_one_le (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖ρ.symbol ε k - 1‖ ≤ ρ.radius * ∑ i : Fin dim, |ε * ↑(k i)|

The scaled-frequency symbol form of the zero-frequency continuity bound.

theorem Anderson4D.integrable_greenFn_mul_etaEpsT4 (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : MeasureTheory.Integrable (fun (z : T4) => greenFn z * ρ.etaEpsT4 ε z) paperMeasure

The Green-weighted covariance density is integrable.

theorem Anderson4D.whiteNoiseFourierScale_eq : NoiseModel.whiteNoiseFourierScale = ((2 * Real.pi) ^ 2)⁻¹

The Lebesgue normalization constant is the explicit inverse square, hence positive.

theorem Anderson4D.whiteNoiseFourierScale_pos : 0 < NoiseModel.whiteNoiseFourierScale

theorem Anderson4D.SmoothCutoff.norm_covarianceModeCoeff (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖ρ.covarianceModeCoeff ε k‖ = NoiseModel.whiteNoiseFourierScale ^ 2 * ‖ρ.symbol ε k‖ ^ 2

Norm of one covariance mode coefficient.

theorem Anderson4D.SmoothCutoff.summable_symbol_sq_mul_invBracket (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => ‖ρ.symbol ε k‖ ^ 2 * (1 + ∑ i : Fin dim, ↑(k i) ^ 2)⁻¹

Summability of the Green-weighted symbol series.

theorem Anderson4D.integral_greenFn_mul_etaEpsT4_eq (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∫ (z : T4), greenFn z * ρ.etaEpsT4 ε z ∂paperMeasure = NoiseModel.whiteNoiseFourierScale ^ 2 * ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 * (1 + ∑ i : Fin dim, ↑(k i) ^ 2)⁻¹

The Green-weighted covariance mass, exactly. In the absolutely convergent covariance Fourier series each mode is weighted by the Green coefficient ⟨k⟩⁻²; this is the two-block analogue of the base-order zero-mode extraction ∫ η_ε = ⟨2π⟩⁻⁴ ‖ρ̂(0)‖² (2π)⁴.

theorem Anderson4D.exists_le_integral_greenFn_mul_etaEpsT4 (ρ : SmoothCutoff) : ∃ (c : ℝ) (εmax : ℝ), 0 < c ∧ 0 < εmax ∧ εmax ≤ 1 / 4 ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ εmax → c / ε ^ 2 ≤ ∫ (z : T4), greenFn z * ρ.etaEpsT4 ε z ∂paperMeasure

ε⁻²-divergence of the Green-weighted covariance mass. All ≈ ε⁻⁴ low modes carry symbol weight ≥ 1/4, and the Green weight ⟨k⟩⁻² sums to ≳ ε⁻² over them. The constant depends only on the mollifier radius.

The two-block schedule of order two

def Anderson4D.idPairingFinTwo : PartialPairing (Fin 2)

The all-singles pairing of a two-point half.

Equations

• Anderson4D.idPairingFinTwo = { toFun := id, involutive := Anderson4D.idPairingFinTwo._proof_1 }

theorem Anderson4D.partialPairing_finTwo_classify (κ : PartialPairing (Fin 2)) : κ = pairingFinTwo ∨ κ = idPairingFinTwo

A pairing of the two-point half is the full swap or all singles.

def Anderson4D.twoBlockContraction : MomentContraction 2

The two-block contraction: both within-half pairings are the full swap, and there are no singles to cross-match.

Equations

• Anderson4D.twoBlockContraction = ⟨Anderson4D.pairingFinTwo, ⟨Anderson4D.pairingFinTwo, Equiv.refl ↥Anderson4D.pairingFinTwo.singles⟩⟩

instance Anderson4D.instIsEmptySubtypeFinOfNatNatMemFinsetSinglesPairingFinTwo : IsEmpty ↥pairingFinTwo.singles

theorem Anderson4D.momentContractionFiber_twoBlock : momentContractionFiber 2 (momentContractionSignature twoBlockContraction) = {twoBlockContraction}

The two-block signature fibre is a singleton: the endpoint signature already determines both within-half pairings, and the swap has no singles.

def Anderson4D.twoBlockScheduleIndex : R324RefinedScheduleIndex 2

The two-block refined schedule index.

Equations

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

theorem Anderson4D.r324RefinedScheduleRepresentative_twoBlock : r324RefinedScheduleRepresentative twoBlockScheduleIndex = twoBlockContraction

The canonical representative of the two-block schedule is the two-block contraction itself: its signature fibre is a singleton.

theorem Anderson4D.momentRefinedContractionFiber_twoBlock : momentRefinedContractionFiber 2 (momentContractionSignature twoBlockContraction) (momentResidualChainSignature twoBlockContraction.fst twoBlockContraction.snd.fst twoBlockContraction.snd.snd) = {twoBlockContraction}

The refined fibre of the two-block schedule is the singleton.

theorem Anderson4D.r324RenormalizedInteriorCore_pairingFinTwo (w : Fin 2 → T4) : r324RenormalizedInteriorCore pairingFinTwo w = ↑(greenFn (w 0 - w 1))

The swap skeleton keeps exactly the raw middle chain edge: the extracted difference factor sits on the erased last edge.

theorem Anderson4D.primitiveCovarianceProduct_twoBlock (ρ : SmoothCutoff) (ε : ℝ) (v : Fin (2 * 2) → T4) : primitiveCovarianceProduct ρ ε 2 (momentCombinedPairing twoBlockContraction.fst twoBlockContraction.snd.fst twoBlockContraction.snd.snd) v = ρ.etaEpsT4 ε (v ⟨0, ⋯⟩ - v ⟨1, ⋯⟩) * ρ.etaEpsT4 ε (v ⟨2, ⋯⟩ - v ⟨3, ⋯⟩)

The two-block covariance product is the product of the two within-half covariance factors.

theorem Anderson4D.norm_r324RefinedEndpointCore_twoBlock (ρ : SmoothCutoff) (ε : ℝ) (v : Fin (2 * 2) → T4) : ‖r324RefinedEndpointCore ρ ε 2 (↑twoBlockScheduleIndex.fst) (↑twoBlockScheduleIndex.snd) (r324RefinedScheduleRepresentative twoBlockScheduleIndex) v‖ = greenFn (v ⟨0, ⋯⟩ - v ⟨1, ⋯⟩) * ρ.etaEpsT4 ε (v ⟨0, ⋯⟩ - v ⟨1, ⋯⟩) * (greenFn (v ⟨2, ⋯⟩ - v ⟨3, ⋯⟩) * ρ.etaEpsT4 ε (v ⟨2, ⋯⟩ - v ⟨3, ⋯⟩))

Pointwise norm of the two-block interior core: the raw Green edge of each half multiplies its own covariance factor on the same relative coordinate.

theorem Anderson4D.integral_twoBlock_half (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : (∫ (w : Fin 2 → T4), greenFn (w 0 - w 1) * ρ.etaEpsT4 ε (w 0 - w 1) ∂MeasureTheory.Measure.pi fun (x : Fin 2) => paperMeasure) = (2 * Real.pi) ^ dim * ∫ (z : T4), greenFn z * ρ.etaEpsT4 ε z ∂paperMeasure

One half of the two-block interior mass: the raw Green edge against its own covariance factor, (2π)⁴ ∫ G η_ε.

theorem Anderson4D.r324RefinedInteriorCoreIntegral_twoBlock (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : r324RefinedInteriorCoreIntegral ρ ε 2 twoBlockScheduleIndex = ((2 * Real.pi) ^ dim * ∫ (z : T4), greenFn z * ρ.etaEpsT4 ε z ∂paperMeasure) ^ 2

The two-block interior core, exactly. The mode-free interior L¹ mass of the two-block schedule is the square of the raw one-block mass (2π)⁴ ∫ G η_ε: no difference factor survives inside the interior core, because the extraction of each swap block sits on the erased terminal chain edge.

theorem Anderson4D.not_r324InteriorCoreLogBudget_two (ρ : SmoothCutoff) (C : ℝ) : ∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 / 4 ∧ 1 ≤ |Real.log ε| ∧ ¬R324InteriorCoreLogBudget ρ ε 2 C

The ε-uniform interior-core budget is false at order two. For every cutoff and every constant, the two-block schedule violates the budget at all sufficiently small scales: its interior mass is ((2π)⁴ ∫ G η_ε)² ≳ ε⁻⁴, while the budget allows only |log ε|.

theorem Anderson4D.not_r324InteriorCoreMajorantBound_two (ρ : SmoothCutoff) {lam : ℝ} (hlam : 0 < lam) (primitiveConstant supportConstant : ℝ) (hsupport : 0 < supportConstant) : ∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 / 4 ∧ 1 ≤ |Real.log ε| ∧ ¬R324InteriorCoreMajorantBound ρ lam ε 2 primitiveConstant supportConstant

Statement 1 itself is false at order two. The mode-free interior inserted-majorant estimate R324InteriorCoreMajorantBound fails for every positive coupling and every choice of constants at all sufficiently small scales: the two-block interior mass ≳ ε⁻⁴/|log ε|² exceeds the integrated majorant ≲ 1/|log ε|.

theorem Anderson4D.r324InteriorCoreLogBudget_two_unsatisfiable (ρ : SmoothCutoff) (C : ℝ) : ¬∀ (ε : ℝ), 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324InteriorCoreLogBudget ρ ε 2 C

The interior-core budget hypothesis is unsatisfiable at order two: no ε-uniform constant discharges it on the admissible scale range, so exists_deterministicMoment_paper_bound_of_logBudget_and_veryHighFrequency and exists_deterministicMoment_paper_bound_of_logBudget_and_highFrequency are vacuous at m = 2.