Cell decomposition of the genuine selected configuration integral

Each member of the restricted canonical selector fibre is now decomposed on the actual five-variable physical measure by the one-open-edge cell partition. This is an exact equality of complex integrals. The selected configuration is not replaced by an unrestricted projected series and no norm is taken.

noncomputable def Anderson4D.SmoothCutoff.r324SelectedPhysicalOpenEdgeCells {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) : FiniteMeasurableCells (R324PhysicalPoint m) (Fin (2 * m) → Z4)

Lift the marked-residual open-edge partition from the internal physical coordinates to the complete (x,y,z,w,v) product.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedPhysicalOpenEdgeCells_index_respects {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (p : R324PhysicalPoint m) : RespectsPairingExcept (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324ResidualMarkedUpperEndpoint π selected) ((r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).index p)

Every physical point is indexed by an open word respecting all unmarked covariance edges.

theorem Anderson4D.SmoothCutoff.r324SelectedHighFullPairingFourierIntegral_eq_openEdgeCells (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) : ρ.r324SelectedHighFullPairingFourierIntegral ε α β κp κm π hexternal hε hε1 hmtrunc ω = ∑ y ∈ (r324SelectedPhysicalOpenEdgeCells κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε).indices, ∫ (p : R324PhysicalPoint m) in (r324SelectedPhysicalOpenEdgeCells κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε).index ⁻¹' {y}, r324Flatten (ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω) p ∂r324PhysicalMeasure m

One exact restricted selected-configuration integral is the finite sum of its genuine open-edge physical cell integrals.