The endpoint harvest: integrating the external character before the norm

This file carries out, for an arbitrary finite entity set F and with the entity sum kept inside, the first of the four external integrations of paper (4.16)–(4.20).

The mechanism

In detIntegrand ρ ε m κ (assemble x y v) the external point x sits in slot 0 of the assembled tuple and is touched by exactly one factor: the head chain edge greenFn (xt 0 - xt 1) = greenFn (x - v 0). That edge is never excluded, because the excluded chain slots are the numbers p.2.val + 1 ≥ 1 of the extracted pairs (detIntegrand_head_not_excluded); every other factor — the remaining chain edges, the renormalization difference factors and the covariance factors — reads the tuple only at slots ≥ 1 (r324DetHeadless_congr). Hence

detIntegrand ρ ε m κ (assemble x y v) = greenFn (x - v 0) * (x-free) (detIntegrand_assemble_eq_head_mul_headless),

and the head factor is the same for every entity: it does not depend on κ, on the right copy, or on the cross pairing. So it factors out of the entity sum (r324CMFlatCore_eq_head_mul_headless) and the x-integration of the summed core is one Green Fourier coefficient:

∫ charT4 α x · core(x, q) dx = translatedGreenMode α (v 0) · headless(q) (integral_charT4_mul_r324CMFlatCore),

whose modulus is exactly ⟨α⟩⁻² — norm_translatedGreenMode — no matter how large the entity set is. This is the harvest the mode-independence theorem r324CMFlatDensity_modes_indep says must happen before any norm is taken: the decay is produced by the oscillation of charT4 α, and taking the modulus of the integrand first destroys it.

The same computation applies verbatim to z, the head of the right copy (assemble z w (v ∘ rightMomentIndex) has the identical head edge greenFn (z - v (rightMomentIndex 0))), giving a second factor ⟨α⟩⁻²; together they are exactly paperFourthOrderModeDecay α, the α half of r324EndpointLoss. The y and w endpoints sit at the last chain slot, which the extracted pairs may replace by a difference factor, so their harvest is a difference of two translated Green modes rather than one — the proved r324EndpointCoefficient shape.

Removing the head chain edge

noncomputable def Anderson4D.r324DetHeadless (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : ℝ

detIntegrand with the head chain edge greenFn (xt 0 - xt 1) deleted. Every remaining factor reads xt only at slots ≥ 1.

Equations

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

theorem Anderson4D.detIntegrand_head_not_excluded {m : ℕ} (κ : PartialPairing (Fin m)) : 0 ∉ List.map (fun (p : Fin m × Fin m) => ↑p.2 + 1) (extract κ)

The head chain slot 0 is never excluded: the excluded slots are the numbers p.2.val + 1 of the extracted pairs, all ≥ 1.

theorem Anderson4D.detIntegrand_eq_head_mul_headless (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : detIntegrand ρ ε m κ xt = greenFn (xt 0 - xt 1) * r324DetHeadless ρ ε m κ xt

The head split. detIntegrand is the head Green edge times an x-free remainder.

theorem Anderson4D.r324DetHeadless_congr (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) {xt xt' : Fin (m + 2) → T4} (h : ∀ (j : Fin (m + 2)), ↑j ≠ 0 → xt j = xt' j) : r324DetHeadless ρ ε m κ xt = r324DetHeadless ρ ε m κ xt'

The headless factor only reads the assembled tuple at slots ≥ 1.

theorem Anderson4D.assemble_eq_of_ne_zero {m : ℕ} (x x' y : T4) (v : Fin m → T4) (j : Fin (m + 2)) (hj : ↑j ≠ 0) : assemble x y v j = assemble x' y v j

Assembled tuples that differ only in the external head point agree at every slot ≥ 1.

theorem Anderson4D.assemble_one {m : ℕ} (hm : 0 < m) (x y : T4) (v : Fin m → T4) : assemble x y v 1 = v ⟨0, hm⟩

The head anchor of an assembled tuple is v 0.

theorem Anderson4D.detIntegrand_assemble_eq_head_mul_headless (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : detIntegrand ρ ε m κ (assemble x y v) = greenFn (x - v ⟨0, hm⟩) * r324DetHeadless ρ ε m κ (assemble y y v)

The head split on an assembled tuple, with the head factor written in the external point x and the head anchor v 0.

The head split of the summed core

noncomputable def Anderson4D.r324CMHeadlessCore (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (F : Finset (MomentContraction m)) (q : R324PhysicalRest m) : ℝ

The summed flat core with the head Green edge of the left copy deleted. It does not depend on the external point x.

Equations

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

theorem Anderson4D.r324CMFlatCore_eq_head_mul_headless (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (F : Finset (MomentContraction m)) (x : T4) (q : R324PhysicalRest m) : r324CMFlatCore ρ ε m F (x, q) = greenFn (x - q.2.2.2 (leftMomentIndex ⟨0, hm⟩)) * r324CMHeadlessCore ρ ε m F q

The head factor is entity independent, so it leaves the entity sum untouched: the summed core is the head Green edge times an x-free remainder. No cancellation inside F is spent.

The harvest

theorem Anderson4D.integral_charT4_mul_r324CMFlatCore (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (α : Z4) (F : Finset (MomentContraction m)) (q : R324PhysicalRest m) : ∫ (x : T4), charT4 α x * ↑(r324CMFlatCore ρ ε m F (x, q)) ∂paperMeasure = translatedGreenMode α (q.2.2.2 (leftMomentIndex ⟨0, hm⟩)) * ↑(r324CMHeadlessCore ρ ε m F q)

The endpoint harvest at x. Integrating the summed core against its external character produces one translated Green Fourier coefficient at the mode α, times the x-free remainder. The entity sum never leaves the integrand.

theorem Anderson4D.norm_integral_charT4_mul_r324CMFlatCore (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (α : Z4) (F : Finset (MomentContraction m)) (q : R324PhysicalRest m) : ‖∫ (x : T4), charT4 α x * ↑(r324CMFlatCore ρ ε m F (x, q)) ∂paperMeasure‖ = paperSecondOrderModeDecay α * |r324CMHeadlessCore ρ ε m F q|

The harvested modulus. The x-integration contributes exactly the second-order mode decay ⟨α⟩⁻², uniformly in the entity set.