Endpoint-preserving periodic reduction

This file joins the periodic cut average from PeriodicQuotient to the endpoint-preserving primitive lattice estimate. The primitive pairings are aggregated by their lower-half cut before the finite cut lift is enlarged to a complete lattice box. This ordering is essential: enlarging one fixed pairing to the complete across-pairing sum and only then summing the source pairings would introduce an extra factorial multiplicity.

Endpoint-supported lattice statistics

noncomputable def Anderson4D.primitiveCanonicalGrid (ε : ℝ) (n : ℕ) : Finset (Fin (2 * n) → Z4)

The common, pairing-independent canonical torus-grid carrier.

Equations

• Anderson4D.primitiveCanonicalGrid ε n = Fintype.piFinset fun (x : Fin (2 * n)) => Anderson4D.torusGrid (Anderson4D.compatibleMeshSize ε)

def Anderson4D.primitiveEndpointSupport {n : ℕ} (hn : 1 ≤ n) (δ R : ℝ) (z w : T4) (y : Fin (2 * n) → Z4) : Prop

Endpoint support transported to an arbitrary lattice lift.

Equations

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

@[implicit_reducible]

noncomputable instance Anderson4D.primitiveEndpointSupport_decidable {n : ℕ} (hn : 1 ≤ n) (δ R : ℝ) (z w : T4) (y : Fin (2 * n) → Z4) : Decidable (primitiveEndpointSupport hn δ R z w y)

Equations

• Anderson4D.primitiveEndpointSupport_decidable hn δ R z w y = Classical.propDecidable (Anderson4D.primitiveEndpointSupport hn δ R z w y)

@[simp]

theorem Anderson4D.primitiveCanonicalEndpointSupported_iff_endpointSupport (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (z w : T4) (y : Fin (2 * n) → Z4) : primitiveCanonicalEndpointSupported ρ ε n hn z w y ↔ primitiveEndpointSupport hn (compatibleMeshSize ε) (1 + 4 * ρ.radius) z w y

noncomputable def Anderson4D.primitiveEndpointSupportedStatistic {n : ℕ} (hn : 1 ≤ n) (A : Finset (Fin (2 * n))) (δ R : ℝ) (z w : T4) (y : Fin (2 * n) → Z4) : ℝ

Sum of all compatible primitive across pairings on one lattice tuple, with the two continuum endpoints kept in their cell neighbourhoods.

Equations

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

theorem Anderson4D.primitiveEndpointSupportedStatistic_nonneg {n : ℕ} (hn : 1 ≤ n) (A : Finset (Fin (2 * n))) (δ R : ℝ) (z w : T4) (y : Fin (2 * n) → Z4) : 0 ≤ primitiveEndpointSupportedStatistic hn A δ R z w y

noncomputable def Anderson4D.primitiveEndpointSupportedLatticeSum (M n : ℕ) (hn : 1 ≤ n) (A : Finset (Fin (2 * n))) (δ R : ℝ) (z w : T4) : ℝ

Endpoint-supported version of the lattice sum in paper (5.5).

Equations

• Anderson4D.primitiveEndpointSupportedLatticeSum M n hn A δ R z w = Anderson4D.latticeChainSum M (2 * n) (Anderson4D.primitiveEndpointSupportedStatistic hn A δ R z w)

Elementary transport through one periodic cut

theorem Anderson4D.r51LatticeReductionWeight_eq_primitiveDirect {n : ℕ} (hn : 1 ≤ n) (y : Fin (2 * n) → Z4) : r51LatticeReductionWeight ⋯ y = primitiveDirectReductionWeight hn y

theorem Anderson4D.primitiveEndpointSupport_r51CutLift_iff {n q : ℕ} [NeZero q] (hn : 1 ≤ n) {δ R : ℝ} (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (z w : T4) (y : Fin (2 * n) → Z4) : (primitiveEndpointSupport hn δ R z w fun (j : Fin (2 * n)) => r51CutLift q c (y j)) ↔ primitiveEndpointSupport hn δ R z w y

theorem Anderson4D.RespectsWord.r51CutLift {m q : ℕ} [NeZero q] {A : Finset (Fin m)} {κ : AcrossPairing A} {y : Fin m → Z4} (hy : RespectsWord A y κ) (c : R51Cut q) : RespectsWord A (fun (j : Fin m) => Anderson4D.r51CutLift q c (y j)) κ

theorem Anderson4D.primitiveCompatibleAcrossPairings_card_le_cutLift {m q : ℕ} [NeZero q] (A : Finset (Fin m)) (y : Fin m → Z4) (c : R51Cut q) : (primitiveCompatibleAcrossPairings A y).card ≤ (primitiveCompatibleAcrossPairings A fun (j : Fin m) => r51CutLift q c (y j)).card

theorem Anderson4D.primitiveCanonicalGrid_coord_abs_le_cellCount {ε : ℝ} (hε : 0 < ε) {n : ℕ} {y : Fin (2 * n) → Z4} (hy : y ∈ primitiveCanonicalGrid ε n) (j : Fin (2 * n)) (i : Fin dim) : |y j i| ≤ compatibleCellCount ε

Aggregate primitive pairings before the box enlargement

noncomputable def Anderson4D.primitiveCutEndpointPairingSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) {q : ℕ} [NeZero q] (c : R51Cut q) (δ R : ℝ) (z w : T4) : ℝ

Literal fixed-cut source sum, retaining the endpoint filter.

Equations

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

theorem Anderson4D.sum_primitiveAcross_cutLift_le_supportedGrid {ε : ℝ} {n q : ℕ} [NeZero q] (hn : 1 ≤ n) {δ R : ℝ} (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (A : Finset (Fin (2 * n))) (z w : T4) : (∑ κ ∈ primitiveAcrossPairingFinset A, ∑ y ∈ primitiveCanonicalCellCarrier ε n (acrossToPartialPairing A κ) with (primitiveEndpointSupport hn δ R z w) y, r51LatticeReductionWeight ⋯ fun (j : Fin (2 * n)) => r51CutLift q c (y j)) ≤ ∑ y ∈ primitiveCanonicalGrid ε n, primitiveEndpointSupportedStatistic hn A δ R z w fun (j : Fin (2 * n)) => r51CutLift q c (y j)

For one cut and one lower-half set, the sum over primitive across pairings is bounded by the endpoint-supported statistic of the lifted tuple. Primitivity is retained and no complete-pairing enlargement is performed here.

theorem Anderson4D.primitiveCutEndpointPairingSum_le_supportedLattice {ε : ℝ} (hε : 0 < ε) {n q : ℕ} [NeZero q] (hn : 1 ≤ n) (hqε : ↑q = compatibleCellCount ε) {δ R : ℝ} (hq : PeriodCompatibleMesh δ ↑q) (c : R51Cut q) (z w : T4) : primitiveCutEndpointPairingSum ε n hn c δ R z w ≤ ↑((3 ^ 4) ^ (2 * n)) * ∑ A : Finset (Fin (2 * n)), primitiveEndpointSupportedLatticeSum (2 * q) n hn A δ R z w

Correct fixed-cut bridge. The source primitive pairings first inject into the all-cuts across carrier. Only after this aggregation is the cut lift enlarged to the common [-2q,2q] lattice box, incurring the uniform 3^(8n) fiber loss exactly once.

The cut average after summing all primitive pairings

noncomputable def Anderson4D.primitivePeriodicEndpointPairingSum (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) (δ R : ℝ) (z w : T4) : ℝ

Periodic endpoint-filtered reduction sum over the complete primitive pairing carrier.

Equations

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

theorem Anderson4D.sum_r51PeriodicReductionFilteredRealSum_endpoint_eq {ε : ℝ} (hε : 0 < ε) (ρ : SmoothCutoff) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) (z w : T4) : ∑ κ ∈ primitiveFullPairings n, r51PeriodicReductionFilteredRealSum ε n hn q (compatibleMeshSize ε) κ (primitiveCopiedEndpointSupported ρ ε n hn z w) = primitivePeriodicEndpointPairingSum ε n hn q (compatibleMeshSize ε) (1 + 4 * ρ.radius) z w

The endpoint-filtered reduction statistic from PeriodicQuotient, summed over primitive pairings, is exactly the real periodic endpoint sum used below.

theorem Anderson4D.r51PeriodicReductionFilteredRealSum_nonneg (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) {δ : ℝ} (hδ : 0 < δ) (κ : PartialPairing (Fin (2 * n))) (P : (Fin (2 * n - 1 + 1) → Z4) → Prop) [DecidablePred P] : 0 ≤ r51PeriodicReductionFilteredRealSum ε n hn q δ κ P

theorem Anderson4D.sum_r51PeriodicReductionFilteredSum_endpoint_eq {ε : ℝ} (hε : 0 < ε) (ρ : SmoothCutoff) (n : ℕ) (hn : 1 ≤ n) (q : ℕ) (z w : T4) : ∑ κ ∈ primitiveFullPairings n, r51PeriodicReductionFilteredSum ε n hn q (compatibleMeshSize ε) κ (primitiveCopiedEndpointSupported ρ ε n hn z w) = ENNReal.ofReal (primitivePeriodicEndpointPairingSum ε n hn q (compatibleMeshSize ε) (1 + 4 * ρ.radius) z w)

ENNReal form of sum_r51PeriodicReductionFilteredRealSum_endpoint_eq, suited to the Tonelli bound for the primitive kernel.

theorem Anderson4D.primitivePeriodicEndpointPairingSum_le_cutAverage {ε δ : ℝ} (hδ : 0 < δ) {n q : ℕ} [NeZero q] (hn : 1 ≤ n) (hq : PeriodCompatibleMesh δ ↑q) (R : ℝ) (z w : T4) : primitivePeriodicEndpointPairingSum ε n hn q δ R z w ≤ Real.exp (12 * (2 * ↑n - 1)) * ((∑ c : R51Cut q, primitiveCutEndpointPairingSum ε n hn c δ R z w) / ↑q ^ 4)

The arithmetic-geometric cut average commutes with the complete primitive-pairing sum.

theorem Anderson4D.primitivePeriodicEndpointPairingSum_le_supportedLattice {ε : ℝ} (hε : 0 < ε) {n q : ℕ} [NeZero q] (hn : 1 ≤ n) (hqε : ↑q = compatibleCellCount ε) {δ : ℝ} (hδ : 0 < δ) (hq : PeriodCompatibleMesh δ ↑q) (R : ℝ) (z w : T4) : primitivePeriodicEndpointPairingSum ε n hn q δ R z w ≤ Real.exp (12 * (2 * ↑n - 1)) * (↑((3 ^ 4) ^ (2 * n)) * ∑ A : Finset (Fin (2 * n)), primitiveEndpointSupportedLatticeSum (2 * q) n hn A δ R z w)

The cut count cancels the averaging denominator after the fixed-cut endpoint-preserving lattice bridge.

Regroup the supported lattice sum by its two endpoints

noncomputable def Anderson4D.primitiveEndpointPairCarrier (M n : ℕ) (hn : 1 ≤ n) : Finset (Z4 × Z4)

Endpoint pairs which actually occur in the finite lattice box.

Equations

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

def Anderson4D.primitiveEndpointPairSupported (δ R : ℝ) (z w : T4) (p : Z4 × Z4) : Prop

Continuum endpoint support written directly on a pair of lattice labels.

Equations

• Anderson4D.primitiveEndpointPairSupported δ R z w p = (z ∈ Anderson4D.latticeCellNeighborhood δ R p.1 ∧ w ∈ Anderson4D.latticeCellNeighborhood δ R p.2)

@[implicit_reducible]

noncomputable instance Anderson4D.primitiveEndpointPairSupported_decidable (δ R : ℝ) (z w : T4) (p : Z4 × Z4) : Decidable (primitiveEndpointPairSupported δ R z w p)

Equations

• Anderson4D.primitiveEndpointPairSupported_decidable δ R z w p = Classical.propDecidable (Anderson4D.primitiveEndpointPairSupported δ R z w p)

noncomputable def Anderson4D.primitiveEndpointBracketSum (M n : ℕ) (hn : 1 ≤ n) (δ R : ℝ) (z w : T4) : ℝ

The geometric endpoint bracket left after the combinatorial sum.

Equations

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

theorem Anderson4D.primitiveEndpointBracketSum_nonneg (M n : ℕ) (hn : 1 ≤ n) (δ R : ℝ) (z w : T4) : 0 ≤ primitiveEndpointBracketSum M n hn δ R z w

theorem Anderson4D.primitiveEndpointPairSupported_bracket_le {δ R : ℝ} (hδ : 0 < δ) (hR : 0 ≤ R) {z w : T4} {p : Z4 × Z4} (hp : primitiveEndpointPairSupported δ R z w p) : latticeBracketInvFourth p.1 p.2 ≤ (9 * (1 + 4 * R ^ 2)) ^ 2 * δ ^ 4 * (torusDistSq (z - w) + δ ^ 2)⁻¹ ^ 2

Uniformly many endpoint labels on one periodic mesh

theorem Anderson4D.torusGridRadius_le_periodCount {δ : ℝ} {q : ℕ} [NeZero q] (hq : PeriodCompatibleMesh δ ↑q) : torusGridRadius δ ≤ ↑q

theorem Anderson4D.torusFloorCell_coord_abs_le_periodCount {δ : ℝ} {q : ℕ} [NeZero q] (hq : PeriodCompatibleMesh δ ↑q) (z : T4) (i : Fin 4) : |torusFloorCell δ z i| ≤ ↑q

theorem Anderson4D.torus_mem_latticeCellNeighborhood_floor {δ : ℝ} (hδ : 0 < δ) (z : T4) : z ∈ latticeCellNeighborhood δ 1 (torusFloorCell δ z)

noncomputable def Anderson4D.primitiveEndpointPeriodCode (q : ℕ) (x a : Z4) : Z4

Period-translation code used by nearestPeriodTranslate.

Equations

• Anderson4D.primitiveEndpointPeriodCode q x a i = round (↑((x - a) i) / ↑q)

theorem Anderson4D.primitiveEndpointPeriodCode_mem_ball_four {q : ℕ} [NeZero q] {x a : Z4} (hx : ∀ (i : Fin dim), |x i| ≤ ↑(2 * q)) (ha : ∀ (i : Fin dim), |a i| ≤ ↑q) : primitiveEndpointPeriodCode q x a ∈ latticeBallNat 0 4

noncomputable def Anderson4D.primitiveEndpointPeriodCenters (q : ℕ) (δ : ℝ) (z : T4) : Finset Z4

The bounded set of period translates which can be nearest to a point of [-2q,2q]⁴ when the canonical anchor lies in [-q,q]⁴.

Equations

• Anderson4D.primitiveEndpointPeriodCenters q δ z = Finset.image (fun (k : Anderson4D.Z4) => Anderson4D.translateCellIndex (↑q) k (Anderson4D.torusFloorCell δ z)) (Anderson4D.latticeBallNat 0 4)

theorem Anderson4D.card_primitiveEndpointPeriodCenters_le (q : ℕ) (δ : ℝ) (z : T4) : (primitiveEndpointPeriodCenters q δ z).card ≤ 10000

noncomputable def Anderson4D.primitiveEndpointLabelCover (q : ℕ) (δ R : ℝ) (z : T4) : Finset Z4

Uniform endpoint-label cover; the radius is the support radius plus the one-cell error of the canonical floor anchor.

Equations

• Anderson4D.primitiveEndpointLabelCover q δ R z = Anderson4D.latticeBallUnion (Anderson4D.primitiveEndpointPeriodCenters q δ z) (R + 1)

theorem Anderson4D.mem_primitiveEndpointLabelCover {q : ℕ} [NeZero q] {δ R : ℝ} (hq : PeriodCompatibleMesh δ ↑q) {z : T4} {x : Z4} (hxbox : ∀ (i : Fin dim), |x i| ≤ ↑(2 * q)) (hx : z ∈ latticeCellNeighborhood δ R x) : x ∈ primitiveEndpointLabelCover q δ R z

theorem Anderson4D.card_primitiveEndpointLabelCover_le {R : ℝ} (hR : 0 ≤ R) (q : ℕ) (δ : ℝ) (z : T4) : ↑(primitiveEndpointLabelCover q δ R z).card ≤ 160000 * (R + 2) ^ 4

theorem Anderson4D.card_primitiveEndpointSupportedPairs_le {q n : ℕ} [NeZero q] (hn : 1 ≤ n) {δ R : ℝ} (hR : 0 ≤ R) (hq : PeriodCompatibleMesh δ ↑q) (z w : T4) : ↑(Finset.filter (primitiveEndpointPairSupported δ R z w) (primitiveEndpointPairCarrier (2 * q) n hn)).card ≤ (160000 * (R + 2) ^ 4) ^ 2

The two endpoint labels range over a uniformly bounded product cover, independently of the period count.

theorem Anderson4D.primitiveEndpointBracketSum_le_globalDecay {q n : ℕ} [NeZero q] (hn : 1 ≤ n) {δ R : ℝ} (hR : 0 ≤ R) (hq : PeriodCompatibleMesh δ ↑q) (z w : T4) : primitiveEndpointBracketSum (2 * q) n hn δ R z w ≤ (160000 * (R + 2) ^ 4) ^ 2 * ((9 * (1 + 4 * R ^ 2)) ^ 2 * δ ^ 4 * (torusDistSq (z - w) + δ ^ 2)⁻¹ ^ 2)

Final geometric estimate for the endpoint bracket sum.

theorem Anderson4D.primitiveEndpointSupport_iff_pairSupported {n : ℕ} (hn : 1 ≤ n) (δ R : ℝ) (z w : T4) (y : Fin (2 * n) → Z4) : primitiveEndpointSupport hn δ R z w y ↔ primitiveEndpointPairSupported δ R z w (y (primitiveEndpointLeft n hn), y (primitiveEndpointRight n hn))

theorem Anderson4D.primitiveEndpointSupportedLatticeSum_eq_endpointPairs (M n : ℕ) (hn : 1 ≤ n) (A : Finset (Fin (2 * n))) (δ R : ℝ) (z w : T4) : primitiveEndpointSupportedLatticeSum M n hn A δ R z w = ∑ p ∈ primitiveEndpointPairCarrier M n hn, if primitiveEndpointPairSupported δ R z w p then primitiveEndpointLatticeSum M n hn A p.1 p.2 else 0

Exact endpoint-fiber decomposition of the supported lattice sum.

noncomputable def Anderson4D.primitiveEndpointUniformCoefficient (C : ℝ) (M n K : ℕ) : ℝ

The endpoint-independent coefficient supplied by the final Hepp-tree assembly.

Equations

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

theorem Anderson4D.primitiveEndpointUniformCoefficient_nonneg {C : ℝ} (hC : 0 ≤ C) (M n K : ℕ) : 0 ≤ primitiveEndpointUniformCoefficient C M n K

theorem Anderson4D.primitiveEndpointLatticeSum_le_coefficient_mul_bracket {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (A : Finset (Fin (2 * n))) (x₀ x₁ : Z4) : primitiveEndpointLatticeSum M n ⋯ A x₀ x₁ ≤ primitiveEndpointUniformCoefficient C M n K * latticeBracketInvFourth x₀ x₁

theorem Anderson4D.primitiveEndpointSupportedLatticeSum_le_bracketSum {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (A : Finset (Fin (2 * n))) (δ R : ℝ) (z w : T4) : primitiveEndpointSupportedLatticeSum M n ⋯ A δ R z w ≤ primitiveEndpointUniformCoefficient C M n K * primitiveEndpointBracketSum M n ⋯ δ R z w

Apply the fixed-endpoint tree estimate after the exact endpoint-fiber decomposition.

theorem Anderson4D.sum_primitiveEndpointSupportedLatticeSum_le {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (δ R : ℝ) (z w : T4) : ∑ A : Finset (Fin (2 * n)), primitiveEndpointSupportedLatticeSum M n ⋯ A δ R z w ≤ ↑(2 ^ (2 * n)) * primitiveEndpointUniformCoefficient C M n K * primitiveEndpointBracketSum M n ⋯ δ R z w

Sum over the 2^(2n) lower-half choices without reintroducing any pairing multiplicity.

theorem Anderson4D.primitivePeriodicEndpointPairingSum_le_globalDecay {C : ℝ} (hC : PermSumEstimate C) {ε : ℝ} (hε : 0 < ε) {n q K : ℕ} [NeZero q] (hn : 2 ≤ n) (hqε : ↑q = compatibleCellCount ε) {δ R : ℝ} (hR : 0 ≤ R) (hq : PeriodCompatibleMesh δ ↑q) (hnL : n ≤ K * (Nat.log 2 (4 * (2 * q)) + 1)) (z w : T4) : primitivePeriodicEndpointPairingSum ε n ⋯ q δ R z w ≤ Real.exp (12 * (2 * ↑n - 1)) * (↑((3 ^ 4) ^ (2 * n)) * (↑(2 ^ (2 * n)) * primitiveEndpointUniformCoefficient C (2 * q) n K * ((160000 * (R + 2) ^ 4) ^ 2 * ((9 * (1 + 4 * R ^ 2)) ^ 2 * δ ^ 4 * (torusDistSq (z - w) + δ ^ 2)⁻¹ ^ 2))))

Complete endpoint-preserving R-51 estimate at the periodic real-sum level. All losses are explicit and the global inserted decay remains visible.

noncomputable def Anderson4D.primitiveR51GlobalDecayBound (C : ℝ) (n q K : ℕ) (δ R : ℝ) (z w : T4) : ℝ

Named right-hand side of the endpoint-preserving periodic R-51 estimate. Naming it keeps the continuum and coupling ledgers independent of the (already closed) Hepp-tree expression.

Equations

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

theorem Anderson4D.primitivePeriodicEndpointPairingSum_le_r51GlobalDecayBound {C : ℝ} (hC : PermSumEstimate C) {ε : ℝ} (hε : 0 < ε) {n q K : ℕ} [NeZero q] (hn : 2 ≤ n) (hqε : ↑q = compatibleCellCount ε) {δ R : ℝ} (hR : 0 ≤ R) (hq : PeriodCompatibleMesh δ ↑q) (hnL : n ≤ K * (Nat.log 2 (4 * (2 * q)) + 1)) (z w : T4) : primitivePeriodicEndpointPairingSum ε n ⋯ q δ R z w ≤ primitiveR51GlobalDecayBound C n q K δ R z w

Return to the continuum primitive integrals

theorem Anderson4D.sum_primitiveInsertedIntegrand_lintegral_le_periodicEndpointPairingSum (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ {q : ℕ} [NeZero q], PeriodCompatibleMesh (compatibleMeshSize ε) ↑q → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; (∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n ⋯ G κ (primitiveAssemble n ⋯ z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ENNReal.ofReal Q * (ENNReal.ofReal farCoeff + ENNReal.ofReal nearCoeff) * ENNReal.ofReal (primitivePeriodicEndpointPairingSum ε n ⋯ q δ R z w)

Sum the cellwise Tonelli estimate over the complete primitive pairing carrier before applying the endpoint-preserving periodic bound. In particular, this theorem does not pay a copy of the all-pairings lattice estimate for each source pairing.

theorem Anderson4D.sum_primitiveInsertedIntegrand_lintegral_le_r51GlobalDecayBound {C : ℝ} (hC : PermSumEstimate C) (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ {q : ℕ} [NeZero q], ↑q = compatibleCellCount ε → ∀ (K : ℕ), n ≤ K * (Nat.log 2 (4 * (2 * q)) + 1) → ∀ (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; (∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n ⋯ G κ (primitiveAssemble n ⋯ z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ENNReal.ofReal Q * (ENNReal.ofReal farCoeff + ENNReal.ofReal nearCoeff) * ENNReal.ofReal (primitiveR51GlobalDecayBound C n q K δ R z w)

Complete inserted R-51 bound at the continuum-integrand level, with all covariance, cell, periodic-cut, endpoint, and Hepp-tree factors kept explicit.

theorem Anderson4D.ofReal_abs_primitiveKernelInserted_le_lintegralSum (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : ENNReal.ofReal |primitiveKernelInserted ρ lam ε n hn G z w| ≤ ENNReal.ofReal (lamEps lam ε ^ (2 * n)) * ∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

The absolute value of the Bochner sum defining the inserted primitive kernel is controlled by the same summed lintegral. This uses only the universal norm bound for the Bochner integral; no sign, integrability, or separate measurability assumption is hidden here.

theorem Anderson4D.ofReal_abs_primitiveKernelInserted_le_r51GlobalDecayBound {C : ℝ} (hC : PermSumEstimate C) (ρ : SmoothCutoff) : ∃ (Ccov : ℝ) (Ccell : ℝ), 0 < Ccov ∧ 0 < Ccell ∧ ∀ (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n G → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ {q : ℕ} [NeZero q], ↑q = compatibleCellCount ε → ∀ (K : ℕ), n ≤ K * (Nat.log 2 (4 * (2 * q)) + 1) → ∀ (lam : ℝ) (z w : T4), have R := 1 + 4 * ρ.radius; have δ := compatibleMeshSize ε; have farCoeff := (12 + 32 * R ^ 2) * (Ccell * (R ^ 2 + R ^ 4)) ^ (2 * n - 2) * terminalRadiusFactor R * δ ^ (4 * n - 4); have nearCoeff := (12 + 32 * R ^ 2) * (Ccell * cellChainRadiusFactor R) ^ (2 * n - 3) * δ ^ (4 * n - 4); have Q := (ε⁻¹ ^ dim * Ccov) ^ n; ENNReal.ofReal |primitiveKernelInserted ρ lam ε n ⋯ G z w| ≤ ENNReal.ofReal (lamEps lam ε ^ (2 * n)) * (ENNReal.ofReal Q * (ENNReal.ofReal farCoeff + ENNReal.ofReal nearCoeff) * ENNReal.ofReal (primitiveR51GlobalDecayBound C n q K δ R z w))

Explicit all-factor inserted-kernel estimate obtained by composing the Bochner norm inequality with the completed endpoint-preserving R-51 reduction.

Recovering the non-inserted kernel

theorem Anderson4D.endpointFactor_mul_abs_primitiveIntegrand_le_inserted (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (z w : T4) (v : Fin (2 * n - 2) → T4) : (ε ^ 2 + torusDistSq (z - w)) * |primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ≤ |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)|

The insertion dominates the squared separation of the two fixed endpoints, pointwise in every internal-variable assignment.

theorem Anderson4D.endpointFactor_mul_sum_primitiveIntegrand_lintegral_le_inserted (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : (ENNReal.ofReal (ε ^ 2 + torusDistSq (z - w)) * ∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) ≤ ∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

Summed lintegral form of the endpoint-insertion comparison.

theorem Anderson4D.ofReal_abs_primitiveKernel_le_lintegralSum (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : ENNReal.ofReal |primitiveKernel ρ lam ε n hn G z w| ≤ ENNReal.ofReal (lamEps lam ε ^ (2 * n)) * ∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

Bochner norm bound for the non-inserted primitive kernel.

theorem Anderson4D.endpointFactor_mul_ofReal_abs_primitiveKernel_le_insertedSum (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : ENNReal.ofReal (ε ^ 2 + torusDistSq (z - w)) * ENNReal.ofReal |primitiveKernel ρ lam ε n hn G z w| ≤ ENNReal.ofReal (lamEps lam ε ^ (2 * n)) * ∑ κ ∈ primitiveFullPairings n, ∫⁻ (v : Fin (2 * n - 2) → T4), ENNReal.ofReal |primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

The ordinary kernel is reduced to the inserted Tonelli sum after multiplication by its endpoint factor.