The head harvest at both copies: the ⟨α⟩⁻⁴ half of the tail ledger

noncomputable def Anderson4D.r324TailInnerMeasure (m : ℕ) : MeasureTheory.Measure (T4 × (Fin (2 * m) → T4))

The measure on the two innermost physical variables (w, v).

Equations

• Anderson4D.r324TailInnerMeasure m = Anderson4D.paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => Anderson4D.paperMeasure)

instance Anderson4D.instSFiniteR324TailInnerMeasure (m : ℕ) : MeasureTheory.SFinite (r324TailInnerMeasure m)

theorem Anderson4D.r324Tail_integral_peel {m : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : R324PhysicalPoint m → E) (hf : MeasureTheory.Integrable f (r324PhysicalMeasure m)) : ∫ (p : R324PhysicalPoint m), f p ∂r324PhysicalMeasure m = ∫ (s : T4 × (Fin (2 * m) → T4)), ∫ (z : T4), ∫ (y : T4), ∫ (x : T4), f (x, y, z, s) ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂r324TailInnerMeasure m

The three outer peels. The physical integral, written with the three external variables x, y, z integrated innermost, in that order. This is the order in which the external characters are harvested.

Both head Green edges removed

noncomputable def Anderson4D.r324CMDoubleHeadlessCore (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (F : Finset (MomentContraction m)) (y w : T4) (v : Fin (2 * m) → T4) : ℝ

The summed flat core with the head chain edge of both copies deleted. Both deleted edges are entity independent, so no cancellation inside F is spent; the result depends only on the two tail external points y, w and the internal variables v.

Equations

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

theorem Anderson4D.r324CMFlatCore_eq_heads_mul_doubleHeadless (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (F : Finset (MomentContraction m)) (x y z : T4) (s : T4 × (Fin (2 * m) → T4)) : r324CMFlatCore ρ ε m F (x, y, z, s) = greenFn (x - s.2 (leftMomentIndex ⟨0, hm⟩)) * (greenFn (z - s.2 (rightMomentIndex ⟨0, hm⟩)) * r324CMDoubleHeadlessCore ρ ε m F y s.1 s.2)

The two-head split of the summed core. Both head Green edges factor out of the entity sum.

Integrability of the character-times-core integrand

theorem Anderson4D.r324Tail_integrable_charCore (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (F : Finset (MomentContraction m)) : MeasureTheory.Integrable (fun (p : R324PhysicalPoint m) => r324ExternalChar m α β p * ↑(r324CMFlatCore ρ ε m F p)) (r324PhysicalMeasure m)

theorem Anderson4D.r324Tail_integrable_absCore (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (F : Finset (MomentContraction m)) : MeasureTheory.Integrable (fun (p : R324PhysicalPoint m) => |r324CMFlatCore ρ ε m F p|) (r324PhysicalMeasure m)

The two head Fourier coefficients

theorem Anderson4D.paperFourthOrderModeDecay_eq_sq (k : Z4) : paperFourthOrderModeDecay k = paperSecondOrderModeDecay k * paperSecondOrderModeDecay k

theorem Anderson4D.translatedGreenMode_eq_paper (k : Z4) (z : T4) : translatedGreenMode k z = charT4 k z * ↑(paperSecondOrderModeDecay k)

noncomputable def Anderson4D.r324TailBetaCoefficient (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (β : Z4) (F : Finset (MomentContraction m)) (s : T4 × (Fin (2 * m) → T4)) : ℂ

The y-Fourier coefficient of the double-headless core: the tail harvest at the left copy, with the entity sum still inside.

Equations

• Anderson4D.r324TailBetaCoefficient ρ ε m β F s = ∫ (y : Anderson4D.T4), Anderson4D.charT4 β y * ↑(Anderson4D.r324CMDoubleHeadlessCore ρ ε m F y s.1 s.2) ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.r324TailHeadHarvest (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (F : Finset (MomentContraction m)) (i : Fin m) : ℂ

The head-harvested integral. What is left of clause B after the two head Green edges have been integrated against their characters: the two head characters now sit at the internal anchors v (leftMomentIndex i) and v (rightMomentIndex i), which is where the external mode α enters the internal covariance sum.

Equations

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

The three inner integrations

theorem Anderson4D.r324Tail_inner_x (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) (y z : T4) (s : T4 × (Fin (2 * m) → T4)) : ∫ (x : T4), r324ExternalChar m α β (x, y, z, s) * ↑(r324CMFlatCore ρ ε m F (x, y, z, s)) ∂paperMeasure = charT4 β y * ↑(r324CMDoubleHeadlessCore ρ ε m F y s.1 s.2) * (translatedGreenMode α (s.2 (leftMomentIndex ⟨0, hm⟩)) * (charT4 (-α) z * ↑(greenFn (z - s.2 (rightMomentIndex ⟨0, hm⟩)))) * charT4 (-β) s.1)

theorem Anderson4D.r324Tail_inner_xy (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) (z : T4) (s : T4 × (Fin (2 * m) → T4)) : ∫ (y : T4), ∫ (x : T4), r324ExternalChar m α β (x, y, z, s) * ↑(r324CMFlatCore ρ ε m F (x, y, z, s)) ∂paperMeasure ∂paperMeasure = r324TailBetaCoefficient ρ ε m β F s * (translatedGreenMode α (s.2 (leftMomentIndex ⟨0, hm⟩)) * (charT4 (-α) z * ↑(greenFn (z - s.2 (rightMomentIndex ⟨0, hm⟩)))) * charT4 (-β) s.1)

theorem Anderson4D.r324Tail_inner_xyz (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) (s : T4 × (Fin (2 * m) → T4)) : ∫ (z : T4), ∫ (y : T4), ∫ (x : T4), r324ExternalChar m α β (x, y, z, s) * ↑(r324CMFlatCore ρ ε m F (x, y, z, s)) ∂paperMeasure ∂paperMeasure ∂paperMeasure = ↑(paperFourthOrderModeDecay α) * (charT4 α (s.2 (leftMomentIndex ⟨0, hm⟩)) * charT4 (-α) (s.2 (rightMomentIndex ⟨0, hm⟩)) * charT4 (-β) s.1 * r324TailBetaCoefficient ρ ε m β F s)

The exact head harvest

theorem Anderson4D.r324Tail_sum_eq_alphaDecay_mul_headHarvest (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) : ∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e = ↑(paperFourthOrderModeDecay α) * r324TailHeadHarvest ρ ε m α β F ⟨0, hm⟩

The head harvest, exactly. The clause-B left-hand side is the fourth-order mode decay ⟨α⟩⁻⁴ times the head-harvested integral. This is an identity, so the remaining decay factors still multiply on: no estimate has been spent, and the entity sum has never left the integrand.

The absolute value side

theorem Anderson4D.r324Tail_absCore_triple (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (hm : 0 < m) (F : Finset (MomentContraction m)) (s : T4 × (Fin (2 * m) → T4)) : ∫ (z : T4), ∫ (y : T4), ∫ (x : T4), |r324CMFlatCore ρ ε m F (x, y, z, s)| ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∫ (y : T4), |r324CMDoubleHeadlessCore ρ ε m F y s.1 s.2| ∂paperMeasure

The three inner integrations of the modulus of the core: the two head Green edges have unit paper mass and are nonnegative, so they disappear.

theorem Anderson4D.r324Tail_integrable_absDouble (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (F : Finset (MomentContraction m)) : MeasureTheory.Integrable (fun (s : T4 × (Fin (2 * m) → T4)) => ∫ (y : T4), |r324CMDoubleHeadlessCore ρ ε m F y s.1 s.2| ∂paperMeasure) (r324TailInnerMeasure m)

theorem Anderson4D.r324Tail_integral_absCore_eq (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (F : Finset (MomentContraction m)) : ∫ (p : R324PhysicalPoint m), |r324CMFlatCore ρ ε m F p| ∂r324PhysicalMeasure m = ∫ (s : T4 × (Fin (2 * m) → T4)), ∫ (y : T4), |r324CMDoubleHeadlessCore ρ ε m F y s.1 s.2| ∂paperMeasure ∂r324TailInnerMeasure m

The physical L¹ norm of the core, with the two head Green edges integrated out.

The modulus corollary

theorem Anderson4D.r324Tail_norm_headHarvest_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) : ‖r324TailHeadHarvest ρ ε m α β F ⟨0, hm⟩‖ ≤ ∫ (p : R324PhysicalPoint m), |r324CMFlatCore ρ ε m F p| ∂r324PhysicalMeasure m

The head harvest is bounded by the clause-A carrier. Dropping the three unimodular characters and the y-oscillation costs nothing beyond the triangle inequality.

theorem Anderson4D.r324Tail_norm_sum_le_fourthOrder_alpha (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (F : Finset (MomentContraction m)) : ‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ paperFourthOrderModeDecay α * ∫ (p : R324PhysicalPoint m), |r324CMFlatCore ρ ε m F p| ∂r324PhysicalMeasure m

The ⟨α⟩⁻⁴ half of the tail ledger, unconditionally. Both head Green edges are entity independent, so both harvests factor out of the entity sum, yielding exactly the clause-A carrier.

theorem Anderson4D.r324Tail_integral_absCore_le {ρ : SmoothCutoff} {K : ℝ} (hA : R324CappedDensityLedger ρ K) {ε : ℝ} (m : ℕ) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hcap : m ≤ truncOrder ε) (F : Finset (MomentContraction m)) : ∫ (p : R324PhysicalPoint m), |r324CMFlatCore ρ ε m F p| ∂r324PhysicalMeasure m ≤ K ^ m * |Real.log ε| ^ (m - 1)

The clause-A carrier bound, in the |core| form.

theorem Anderson4D.r324Tail_norm_sum_le_alphaLedger {ρ : SmoothCutoff} {K : ℝ} (hA : R324CappedDensityLedger ρ K) {ε : ℝ} (m : ℕ) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hcap : m ≤ truncOrder ε) (F : Finset (MomentContraction m)) : ‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * paperFourthOrderModeDecay α

The ⟨α⟩⁻⁴ ledger. Clause B graded by the α-endpoint decay alone, for an arbitrary entity set and every m ≥ 2.