Direct Fourier evaluation of the four endpoint legs, per refined fibre

The endpoint-first Fubini normal form of a refined physical fibre evaluates all four external endpoints directly against their surviving Green legs — in particular the incoming endpoint, whose flag is false by definition, so the .directFourier incoming branch is realized unconditionally, with no case split on ⟨0, hm⟩ ∈ finalActive. This file scalarizes that normal form: the weighted refined physical integral is bounded, for every refined schedule index, by the full paper mode decay 16⟨α⟩⁻⁴⟨β⟩⁻⁴ times the mode-independent L¹ norm of the interior signed core. On the doubly-direct outgoing branch the universal factor 16 improves to 1.

theorem Anderson4D.norm_r324EndpointFirstRefinedCoreIntegrand_eq (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : ‖r324EndpointFirstRefinedCoreIntegrand ρ ε m hm α β p v‖ = r324FourEndpointCoefficientWeight α β (r324ContractionEndpointAnchors hm (r324RefinedScheduleRepresentative p) v) (r324ContractionEndpointFlags (r324RefinedScheduleRepresentative p)) * ‖r324RefinedEndpointCore ρ ε m (↑p.fst) (↑p.snd) (r324RefinedScheduleRepresentative p) v‖

Pointwise scalarization of the endpoint-first integrand: its norm is exactly the four-endpoint Fourier weight times the interior core norm.

theorem Anderson4D.exists_norm_sum_primitiveCovarianceProduct_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (v : Fin (2 * m) → T4), ‖∑ e ∈ momentRefinedContractionFiber m s r, ↑(primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v)‖ ≤ B

The finite primitive-pairing covariance sum of one refined fibre is uniformly bounded on the doubled configuration space.

theorem Anderson4D.integrable_norm_r324RefinedEndpointCore (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) : MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => ‖r324RefinedEndpointCore ρ ε m s r e₀ v‖) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

The interior signed core of a refined fibre has integrable norm on the doubled configuration space: the two endpoint-free Green profiles are jointly integrable and the finite primitive-pairing covariance sum is uniformly bounded.

noncomputable def Anderson4D.r324RefinedInteriorCoreIntegral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (p : R324RefinedScheduleIndex m) : ℝ

Mode-independent interior L¹ mass of one refined fibre.

Equations

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

theorem Anderson4D.r324RefinedInteriorCoreIntegral_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (p : R324RefinedScheduleIndex m) : 0 ≤ r324RefinedInteriorCoreIntegral ρ ε m p

theorem Anderson4D.norm_r324RefinedPhysicalIntegral_le_modeDecay_mul_interiorCore (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (p : R324RefinedScheduleIndex m) : ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * r324RefinedInteriorCoreIntegral ρ ε m p

Scalarized direct Fourier evaluation, all refined fibres. The four endpoint legs (the incoming ones with flag false, i.e. the .directFourier evaluation, and the outgoing ones with their shortcut flag) are Fourier-evaluated directly, yielding the complete paper mode decay 16⟨α⟩⁻⁴⟨β⟩⁻⁴ in front of the mode-independent interior mass. No case split on ⟨0, hm⟩ ∈ finalActive is needed: this bound holds for every refined schedule index.

theorem Anderson4D.norm_r324EndpointCoefficient_false (k : Z4) (u v : T4) : ‖r324EndpointCoefficient k u v false‖ = paperSecondOrderModeDecay k

A flagless endpoint leg is Fourier-evaluated exactly: its coefficient norm is the Euclidean Green multiplier itself.

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

theorem Anderson4D.r324FourEndpointCoefficientWeight_eq_of_direct (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (h1 : flags 1 = false) (h3 : flags 3 = false) (h0 : flags 0 = false) (h2 : flags 2 = false) : r324FourEndpointCoefficientWeight α β anchors flags = paperFourthOrderModeDecay α * paperFourthOrderModeDecay β

With all four flags false (both incoming legs are always direct; both outgoing legs non-shortcut) the four-endpoint weight is exactly ⟨α⟩⁻⁴⟨β⟩⁻⁴, with no factor 16.

theorem Anderson4D.norm_r324RefinedPhysicalIntegral_le_modeDecay_mul_interiorCore_of_direct (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (p : R324RefinedScheduleIndex m) (hout1 : r324OutgoingIsShortcut (r324RefinedScheduleRepresentative p).fst = false) (hout2 : r324OutgoingIsShortcut (r324RefinedScheduleRepresentative p).snd.fst = false) : ‖r324RefinedPhysicalIntegral ρ ε m α β p‖ ≤ paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * r324RefinedInteriorCoreIntegral ρ ε m p

Doubly-direct branch strengthening. When both outgoing legs of the representative are non-shortcut (the incoming legs are direct by definition), the universal factor 16 disappears: the refined physical integral is bounded by the exact ⟨α⟩⁻⁴⟨β⟩⁻⁴ decay times the interior mass.