Aggregate endpoint Fourier loss for R-324

Paper Section 4.2, Step 2 first collapses all within-half primitive intervals while the physical integrand is signed. In the decay branch, Step 4 then integrates each external Green leg before taking the absolute value. Every leg contributes its exact Green Fourier coefficient. If the endpoint belongs to a collapsed interval, the remaining phase difference costs a factor at most two; passing from the inserted primitive estimate back to the ordinary one costs ε⁻². We uniformly pay that latter cost also in the easy branch.

This file isolates the resulting bookkeeping from both the primitive-block product reindexing and the central high-frequency routing. In particular, the four actual Green coefficients aggregate directly to 16 * r324EndpointLoss; no endpoint-decay inequality is left for the final countable-routing caller to postulate. Its endpoint-separated identities are also usable as exact Fubini normal forms, but their pointwise norm bounds must not be moved in front of the signed interval collapses.

noncomputable def Anderson4D.r324EndpointBranchCost (ε : ℝ) (shortcut : Bool) : ℝ

Cost of one external endpoint. shortcut = true is the branch in which an extracted difference reaches that endpoint.

Equations

• Anderson4D.r324EndpointBranchCost ε shortcut = (if shortcut = true then 2 else 1) * ε⁻¹ ^ 2

theorem Anderson4D.r324EndpointBranchCost_nonneg (ε : ℝ) (shortcut : Bool) : 0 ≤ r324EndpointBranchCost ε shortcut

theorem Anderson4D.r324EndpointBranchCost_le (ε : ℝ) (shortcut : Bool) : r324EndpointBranchCost ε shortcut ≤ 2 * ε⁻¹ ^ 2

Both endpoint branches are controlled by the same explicit uniform loss.

noncomputable def Anderson4D.r324EndpointFourierWeight (ε : ℝ) (k : Z4) (shortcut : Bool) : ℝ

One actual external Green Fourier coefficient, with the explicit ordinary-versus-inserted branch cost attached.

Equations

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

theorem Anderson4D.r324EndpointFourierWeight_nonneg (ε : ℝ) (k : Z4) (shortcut : Bool) : 0 ≤ r324EndpointFourierWeight ε k shortcut

theorem Anderson4D.r324EndpointFourierWeight_le (ε : ℝ) (k : Z4) (shortcut : Bool) : r324EndpointFourierWeight ε k shortcut ≤ 2 * ε⁻¹ ^ 2 * paperSecondOrderModeDecay k

A single endpoint keeps the exact Euclidean Japanese-bracket Green decay.

@[reducible, inline]

abbrev Anderson4D.R324EndpointFlags : Type

The four external endpoint flags, in (x,y,z,w) order.

Equations

• Anderson4D.R324EndpointFlags = (Fin 4 → Bool)

noncomputable def Anderson4D.r324FourEndpointFourierWeight (ε : ℝ) (α β : Z4) (flags : R324EndpointFlags) : ℝ

Product of the four concrete endpoint Fourier weights. The two left copy endpoints carry α, and the two right copy endpoints carry β.

Equations

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

theorem Anderson4D.r324FourEndpointFourierWeight_nonneg (ε : ℝ) (α β : Z4) (flags : R324EndpointFlags) : 0 ≤ r324FourEndpointFourierWeight ε α β flags

theorem Anderson4D.r324FourEndpointFourierWeight_le (ε : ℝ) (α β : Z4) (flags : R324EndpointFlags) : r324FourEndpointFourierWeight ε α β flags ≤ 16 * r324EndpointLoss ε α β

Four genuine Green Fourier integrations, four uniform ε⁻² sacrifices, and at most four factors of two give precisely the paper's endpoint loss up to the universal factor 16.

noncomputable def Anderson4D.r324EndpointWeightedBudget (ε : ℝ) (α β : Z4) (baseWeight : ℕ → ℝ) (flags : ℕ → R324EndpointFlags) : ℝ

Endpoint-weighted countable budget before the central frequency decay is applied.

Equations

• Anderson4D.r324EndpointWeightedBudget ε α β baseWeight flags = ∑' (a : ℕ), baseWeight a * Anderson4D.r324FourEndpointFourierWeight ε α β (flags a)

theorem Anderson4D.r324EndpointWeightedBudget_le (ε : ℝ) (α β : Z4) (baseWeight : ℕ → ℝ) (flags : ℕ → R324EndpointFlags) (hbase : Summable baseWeight) (hbaseNonneg : ∀ (a : ℕ), 0 ≤ baseWeight a) : r324EndpointWeightedBudget ε α β baseWeight flags ≤ (16 * ∑' (a : ℕ), baseWeight a) * r324EndpointLoss ε α β

Direct countable aggregate form used by the routing construction. The endpoint bound is proved here from the four concrete Fourier coefficients; downstream code only supplies the endpoint-free summable base weights.

Concrete Fourier integration of a Green-tree endpoint

theorem Anderson4D.integral_char_mul_increasingTreeGreenProduct_snoc {n : ℕ} (parent : IncreasingTreeParent (n + 1)) (v : Fin (n + 1) → T4) (k : Z4) : ∫ (y : T4), charT4 k y * increasingTreeGreenProduct parent (Fin.snoc v y) ∂paperMeasure = translatedGreenMode k (v parent.last) * increasingTreeGreenProduct parent.init v

The terminal vertex of every expanded increasing Green tree is a leaf. Its Fourier integration therefore factors exactly into one translated Green coefficient and the tree with that leaf removed.

theorem Anderson4D.norm_translatedGreenMode (k : Z4) (z : T4) : ‖translatedGreenMode k z‖ = paperSecondOrderModeDecay k

theorem Anderson4D.norm_integral_char_mul_increasingTreeGreenProduct_snoc {n : ℕ} (parent : IncreasingTreeParent (n + 1)) (v : Fin (n + 1) → T4) (k : Z4) : ‖∫ (y : T4), charT4 k y * increasingTreeGreenProduct parent (Fin.snoc v y) ∂paperMeasure‖ = paperSecondOrderModeDecay k * ‖increasingTreeGreenProduct parent.init v‖

Norm form of the concrete leaf integration.

Endpoint-first coefficients, before taking absolute values

noncomputable def Anderson4D.r324OutgoingEndpointKernel (u v : T4) (shortcut : Bool) (y : T4) : ℂ

An external Green leg, with the optional endpoint difference which is created when that leg belongs to an extracted interval. The orientation is the one occurring at the right endpoint of a deterministic profile.

Equations

• Anderson4D.r324OutgoingEndpointKernel u v shortcut y = ↑(Anderson4D.greenFn (u - y)) - if shortcut = true then ↑(Anderson4D.greenFn (v - y)) else 0

noncomputable def Anderson4D.r324IncomingEndpointKernel (u v : T4) (shortcut : Bool) (x : T4) : ℂ

The corresponding incoming external Green leg.

Equations

• Anderson4D.r324IncomingEndpointKernel u v shortcut x = ↑(Anderson4D.greenFn (x - u)) - if shortcut = true then ↑(Anderson4D.greenFn (x - v)) else 0

noncomputable def Anderson4D.r324EndpointCoefficient (k : Z4) (u v : T4) (shortcut : Bool) : ℂ

Fourier coefficient of either orientation of an endpoint leg.

Equations

• Anderson4D.r324EndpointCoefficient k u v shortcut = Anderson4D.translatedGreenMode k u - if shortcut = true then Anderson4D.translatedGreenMode k v else 0

theorem Anderson4D.integral_char_mul_r324IncomingEndpointKernel (k : Z4) (u v : T4) (shortcut : Bool) : ∫ (x : T4), charT4 k x * r324IncomingEndpointKernel u v shortcut x ∂paperMeasure = r324EndpointCoefficient k u v shortcut

theorem Anderson4D.integral_char_mul_r324OutgoingEndpointKernel (k : Z4) (u v : T4) (shortcut : Bool) : ∫ (y : T4), charT4 k y * r324OutgoingEndpointKernel u v shortcut y ∂paperMeasure = r324EndpointCoefficient k u v shortcut

Reversing the Green argument does not change the endpoint Fourier coefficient, because the Green kernel is even.

theorem Anderson4D.norm_r324EndpointCoefficient_le (k : Z4) (u v : T4) (shortcut : Bool) : ‖r324EndpointCoefficient k u v shortcut‖ ≤ (if shortcut = true then 2 else 1) * paperSecondOrderModeDecay k

The optional endpoint difference costs at most a factor two, while retaining the exact Euclidean Green multiplier.

theorem Anderson4D.paperSecondOrderModeDecay_neg (k : Z4) : paperSecondOrderModeDecay (-k) = paperSecondOrderModeDecay k

@[reducible, inline]

abbrev Anderson4D.R324EndpointAnchors : Type

The four endpoint anchors for (x,y,z,w). The first coordinate is the ordinary endpoint and the second is the subtraction anchor.

Equations

• Anderson4D.R324EndpointAnchors = (Fin 4 → Anderson4D.T4 × Anderson4D.T4)

noncomputable def Anderson4D.r324FourEndpointCoefficientWeight (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) : ℝ

Product of the four genuine endpoint-first Fourier coefficients, in the exact mode order (α,β,-α,-β) of (4.18).

Equations

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

theorem Anderson4D.r324FourEndpointCoefficientWeight_nonneg (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) : 0 ≤ r324FourEndpointCoefficientWeight α β anchors flags

theorem Anderson4D.r324FourEndpointCoefficientWeight_le (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) : r324FourEndpointCoefficientWeight α β anchors flags ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β

Fourier integration before absolute values gives the full ⟨α⟩⁻⁴⟨β⟩⁻⁴ endpoint decay. At most four endpoint differences account for the universal factor 16.

noncomputable def Anderson4D.r324SacrificedEndpointCoefficientWeight (ε : ℝ) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) : ℝ

The four possible ordinary-versus-inserted sacrifices cost exactly ε⁻⁸; this is kept separate from the genuine Fourier coefficient.

Equations

• Anderson4D.r324SacrificedEndpointCoefficientWeight ε α β anchors flags = ε⁻¹ ^ 8 * Anderson4D.r324FourEndpointCoefficientWeight α β anchors flags

theorem Anderson4D.r324SacrificedEndpointCoefficientWeight_le (ε : ℝ) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) : r324SacrificedEndpointCoefficientWeight ε α β anchors flags ≤ 16 * r324EndpointLoss ε α β

Exact four-leg integration for a grouped collapsed core

noncomputable def Anderson4D.r324EndpointSeparatedIntegrand (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℂ) (x y z w : T4) : ℂ

Four separated endpoint legs multiplying an arbitrary core which is already summed over the relevant primitive-pairing fibre. The nesting is chosen to match the (x,y,z,w) integral order in (4.18).

Equations

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

theorem Anderson4D.integral_r324EndpointSeparatedIntegrand (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℂ) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β anchors flags core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = r324EndpointCoefficient α (anchors 0).1 (anchors 0).2 (flags 0) * (r324EndpointCoefficient β (anchors 1).1 (anchors 1).2 (flags 1) * (r324EndpointCoefficient (-α) (anchors 2).1 (anchors 2).2 (flags 2) * (r324EndpointCoefficient (-β) (anchors 3).1 (anchors 3).2 (flags 3) * core)))

Endpoint-first identity. The four external variables are integrated before any norm is taken. The core may already contain an entire primitive-pairing/configuration fibre, so this lemma does not move an absolute value through the cancellation required by Proposition 4.1.

theorem Anderson4D.norm_integral_r324EndpointSeparatedIntegrand (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℂ) : ‖∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β anchors flags core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure‖ = r324FourEndpointCoefficientWeight α β anchors flags * ‖core‖

Norm form of the endpoint-first identity.

theorem Anderson4D.sacrificed_norm_integral_r324EndpointSeparatedIntegrand_le (ε : ℝ) (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℂ) : ε⁻¹ ^ 8 * ‖∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), r324EndpointSeparatedIntegrand α β anchors flags core x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure‖ ≤ 16 * r324EndpointLoss ε α β * ‖core‖

After the four ordinary-versus-inserted sacrifices, the exact grouped endpoint-first term is controlled by the paper's endpoint loss.