Exact selector-fibre bridge for R-324 Fourier configurations

This module works at the exact full-pairing Fourier-series boundary. Zero integrated configurations are deleted, the remaining configurations are partitioned by their canonical first-large cross slot, and only the selected covariance mode of each member is rewritten through its own high-mode indicator.

The selector fibres remain restricted throughout. They are not enlarged to the unrestricted r324ProjectedCovarianceC series, and no norm is taken before the exact partition. Thus this file supplies an algebraic bridge for a later primitive-fibre consumer; it does not claim a termwise absolute-value reduction or an equality with the unrestricted one-projected covariance product.

Removing zero terms without changing a summable series

theorem Anderson4D.SmoothCutoff.tsum_eq_tsum_nonzero_subtype {Ω : Type u_1} (term : Ω → ℂ) (hterm : Summable term) : ∑' (ω : Ω), term ω = ∑' (ω : { ω : Ω // term ω ≠ 0 }), term ↑ω

A summable series is unchanged when it is restricted to the subtype of indices carrying nonzero terms.

Replacing only the selected configuration factor

noncomputable def Anderson4D.SmoothCutoff.r324SelectedHighPairModeFactor (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) (j : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card) : ℂ

One pair-mode factor in which precisely the selected genuine pair index is passed through the high-mode indicator. Every other pair mode is left literally unchanged.

Equations

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

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

Product of the actual fixed Fourier modes with only the selected factor guarded by its high-mode indicator.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedHighPairModeFactor_eq (ρ : 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 π) (v : Fin (2 * m) → T4) (j : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card) : ρ.r324SelectedHighPairModeFactor ε ‖z4EuclideanFrequency (α + β)‖ κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) v j = ρ.r324PairModeTerm ε (momentCombinedPairing κp κm π) v j (↑ω j)

On an actual nonzero configuration, every pair factor is unchanged after guarding its own canonical selected pair by the high-mode indicator.

theorem Anderson4D.SmoothCutoff.r324SelectedHighCovarianceConfigurationTerm_eq (ρ : 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 π) (v : Fin (2 * m) → T4) : ρ.r324SelectedHighCovarianceConfigurationTerm ε ‖z4EuclideanFrequency (α + β)‖ κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) v = ρ.r324CovarianceFourierConfigurationTerm ε (momentCombinedPairing κp κm π) v ↑ω

Hence the whole fixed-mode covariance product is unchanged.

Pointwise and integrated selected-indicator terms

noncomputable def Anderson4D.SmoothCutoff.r324SelectedHighFullPairingFourierIntegrand (ρ : 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 π) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The full physical Fourier integrand with only its own canonical selected pair factor guarded by the high-mode indicator.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedHighFullPairingFourierIntegrand_eq (ρ : 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 π) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω x y z w v = ρ.r324FullPairingFourierIntegrand ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ (↑ω) x y z w v

Guarding the canonical selected mode does not change the original full-pairing Fourier integrand.

noncomputable def Anderson4D.SmoothCutoff.r324SelectedHighFullPairingFourierIntegral (ρ : 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 π) : ℂ

Physical integral of one canonically selected high-indicator configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedHighFullPairingFourierIntegral_eq (ρ : 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 ω = ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ ↑ω

Every original nonzero integrated Fourier term is exactly its own selected high-indicator term.

Exact zero deletion and selector-fibre partition

theorem Anderson4D.SmoothCutoff.summable_r324FullPairingFourierIntegral (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Summable fun (q : R324CombinedFourierConfiguration κp κm π) => ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q

Integrated full-pairing Fourier configurations form a summable series.

theorem Anderson4D.SmoothCutoff.tsum_r324FullPairingFourierIntegral_eq_nonzero (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : ∑' (q : R324CombinedFourierConfiguration κp κm π), ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q = ∑' (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π), ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ ↑ω

Zero integrated configurations may be deleted from the actual full-pairing Fourier series.

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324SelectedCrossSlotConfigurationFiber (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (i : R324ResidualCovarianceSlot κp) : Type

The exact fibre of nonzero configurations whose canonical first-large selector is the given cross slot.

Equations

• ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i = ↑(ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ⁻¹' {i})

theorem Anderson4D.SmoothCutoff.tsum_nonzero_r324FullPairingFourierIntegral_eq_selectorFibres (ρ : 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 π), ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ ↑ω = ∑ i : R324ResidualCovarianceSlot κp, ∑' (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i), ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ ↑↑ω

Nonzero configurations partition without overlap or omission into the fibres of the canonical selected cross-slot function.

theorem Anderson4D.SmoothCutoff.tsum_r324FullPairingFourierIntegral_eq_selectedHighFibres (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : ∑' (q : R324CombinedFourierConfiguration κp κm π), ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q = ∑ i : R324ResidualCovarianceSlot κp, ∑' (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i), ρ.r324SelectedHighFullPairingFourierIntegral ε α β κp κm π hexternal hε hε1 hmtrunc ↑ω

Exact configuration-series bridge: after deleting zero terms and partitioning by the canonical selector, each member is replaced only by its own selected high-indicator integral.

theorem Anderson4D.SmoothCutoff.integral_momentFullPairingPhysicalIntegrand_eq_selectedHighFibres (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : ∫ (p : R324PhysicalPoint m), r324Flatten (momentFullPairingPhysicalIntegrand ρ ε m α β ⟨momentCombinedPairing κp κm π, ⋯⟩) p ∂r324PhysicalMeasure m = ∑ i : R324ResidualCovarianceSlot κp, ∑' (ω : ρ.R324SelectedCrossSlotConfigurationFiber ε α β κp κm π hexternal hε hε1 hmtrunc i), ρ.r324SelectedHighFullPairingFourierIntegral ε α β κp κm π hexternal hε hε1 hmtrunc ↑ω

The real full-pairing physical integral, not an abstract routing predicate, is exactly the finite sum of its restricted canonical selected-slot high-indicator fibres.