Endpoint-first physical-integral bridge for R-324

This file records an exact Fubini-reordered normal form in which the four raw external Green legs are integrated before the internal variables. It is not the literal proof order of paper Section 4.2: Step 2 first performs the signed within-half primitive-interval collapses, and Step 4 integrates the endpoint variables after those collapses and before taking absolute values. The equalities here are useful audit identities, but do not by themselves supply a Phase-A iterator.

theorem Anderson4D.r324RefinedPhysicalIntegral_eq_integral_refinedEndpointCoefficient (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (p : R324RefinedScheduleIndex m) : r324RefinedPhysicalIntegral ρ ε m α β p = ∫ (v : Fin (2 * m) → T4), r324RefinedEndpointCoefficient ρ ε m α β (↑p.fst) (↑p.snd) v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Fubini moves the internal variables in front of the four endpoint integrals. No norm or triangle inequality has yet been used.

noncomputable def Anderson4D.r324EndpointFirstRefinedCoreIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : ℂ

The exact endpoint-first integrand associated with a realized refined schedule. Its final factor is still the signed sum over all primitive pairings in that refined fibre.

Equations

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

theorem Anderson4D.r324RefinedEndpointCoefficient_eq_endpointFirstRefinedCoreIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : r324RefinedEndpointCoefficient ρ ε m α β (↑p.fst) (↑p.snd) v = r324EndpointFirstRefinedCoreIntegrand ρ ε m hm α β p v

Pointwise endpoint separation after the four endpoint integrations.

theorem Anderson4D.r324RefinedPhysicalIntegral_eq_integral_endpointFirstRefinedCore (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 0 < m) (α β : Z4) (p : R324RefinedScheduleIndex m) : r324RefinedPhysicalIntegral ρ ε m α β p = ∫ (v : Fin (2 * m) → T4), r324EndpointFirstRefinedCoreIntegrand ρ ε m hm α β p v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Exact endpoint-first normal form of a realized refined physical fibre. This is an auxiliary Fubini normal form; the main signed Phase-A route acts on the original full physical integral.