Endpoint-first factorization on a selected R-324 cell

The selected open-edge cells constrain only the internal doubled tuple. We first move that restriction outside the four endpoint integrals, then evaluate those Fourier integrals exactly. Thus the two ⟨α⟩⁻⁴ ⟨β⟩⁻⁴ endpoint factors are retained before any norm is taken.

def Anderson4D.SmoothCutoff.r324SelectedMomentContraction {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : MomentContraction m

The contraction triple determined by the displayed left, right, and cross pairing data.

Equations

• Anderson4D.SmoothCutoff.r324SelectedMomentContraction κp κm π = ⟨κp, ⟨κm, π⟩⟩

noncomputable def Anderson4D.SmoothCutoff.r324SelectedEndpointCore (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (v : Fin (2 * m) → T4) : ℂ

Interior core of one genuine canonically selected Fourier configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedHighFullPairingFourierIntegrand_eq_endpointSeparated (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω x y z w v = r324EndpointSeparatedIntegrand α β (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v) (r324ContractionEndpointFlags (r324SelectedMomentContraction κp κm π)) (ρ.r324SelectedEndpointCore ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ‖z4EuclideanFrequency (α + β)‖ v) x y z w

Pointwise endpoint-separated form of a selected fixed configuration.

def Anderson4D.SmoothCutoff.r324SelectedInternalCell {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : Set (Fin (2 * m) → T4)

The genuine measurable internal cell selected by one open-edge word.

Equations

• Anderson4D.SmoothCutoff.r324SelectedInternalCell κp κm π selected ε hε cell = (Anderson4D.r324MarkedResidualOpenEdgeCells κp κm π selected ε hε).index ⁻¹' {cell}

theorem Anderson4D.SmoothCutoff.measurableSet_r324SelectedInternalCell {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : MeasurableSet (r324SelectedInternalCell κp κm π selected ε hε cell)

theorem Anderson4D.SmoothCutoff.r324SelectedPhysicalCell_eq_internal_preimage {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : (r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).index ⁻¹' {cell} = r324InternalCoordinate ⁻¹' r324SelectedInternalCell κp κm π selected ε hε cell

The full physical cell fibre is literally the preimage of the corresponding internal cell.

theorem Anderson4D.SmoothCutoff.integral_r324SelectedHigh_on_cell_eq_endpointCoefficients (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (cell : Fin (2 * m) → Z4) : ∫ (p : R324PhysicalPoint m) in (r324SelectedPhysicalOpenEdgeCells κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε).index ⁻¹' {cell}, r324Flatten (ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω) p ∂r324PhysicalMeasure m = ∫ (v : Fin (2 * m) → T4) in r324SelectedInternalCell κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε cell, r324EndpointCoefficient α (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 0).1 (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 0).2 (r324ContractionEndpointFlags (r324SelectedMomentContraction κp κm π) 0) * (r324EndpointCoefficient β (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 1).1 (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 1).2 (r324ContractionEndpointFlags (r324SelectedMomentContraction κp κm π) 1) * (r324EndpointCoefficient (-α) (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 2).1 (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 2).2 (r324ContractionEndpointFlags (r324SelectedMomentContraction κp κm π) 2) * (r324EndpointCoefficient (-β) (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 3).1 (r324ContractionEndpointAnchors hm (r324SelectedMomentContraction κp κm π) v 3).2 (r324ContractionEndpointFlags (r324SelectedMomentContraction κp κm π) 3) * ρ.r324SelectedEndpointCore ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ‖z4EuclideanFrequency (α + β)‖ v))) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Exact endpoint-first formula for one genuine selected cell integral.