Frequency conservation for R-324 Fourier configurations

The Fourier configuration expansion becomes useful only after recording the exact conservation law hidden in the physical integral. We translate all variables in the left parametrix copy by a common torus element. Haar invariance fixes the integral, while its character multiplier is α + β plus the signed sum of the assigned covariance modes. Hence a nonzero configuration integral satisfies the required conservation law.

Character algebra in the spatial argument

@[simp]

theorem Anderson4D.charT4_add_argument (k : Z4) (x y : T4) : charT4 k (x + y) = charT4 k x * charT4 k y

@[simp]

theorem Anderson4D.charT4_neg_argument (k : Z4) (x : T4) : charT4 k (-x) = charT4 (-k) x

@[simp]

theorem Anderson4D.charT4_sub_argument (k : Z4) (x y : T4) : charT4 k (x - y) = charT4 k x * charT4 (-k) y

Translating exactly the left physical copy

noncomputable def Anderson4D.r324LeftInternalTranslateMeasurableEquiv (m : ℕ) (a : T4) : (Fin (2 * m) → T4) ≃ᵐ (Fin (2 * m) → T4)

Translate the internal coordinates belonging to the left copy and leave the right-copy coordinates fixed.

Equations

• Anderson4D.r324LeftInternalTranslateMeasurableEquiv m a = MeasurableEquiv.piCongrRight fun (i : Fin (2 * m)) => if ↑i < m then MeasurableEquiv.addRight a else MeasurableEquiv.refl Anderson4D.T4

@[simp]

theorem Anderson4D.r324LeftInternalTranslateMeasurableEquiv_apply (m : ℕ) (a : T4) (v : Fin (2 * m) → T4) (i : Fin (2 * m)) : (r324LeftInternalTranslateMeasurableEquiv m a) v i = if ↑i < m then v i + a else v i

noncomputable def Anderson4D.r324TranslateLeftPhysicalMeasurableEquiv (m : ℕ) (a : T4) : R324PhysicalPoint m ≃ᵐ R324PhysicalPoint m

Simultaneously translate x, y, and all left internal coordinates.

Equations

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

@[simp]

theorem Anderson4D.r324TranslateLeftPhysicalMeasurableEquiv_apply (m : ℕ) (a : T4) (p : R324PhysicalPoint m) : (r324TranslateLeftPhysicalMeasurableEquiv m a) p = (p.1 + a, p.2.1 + a, p.2.2.1, p.2.2.2.1, fun (i : Fin (2 * m)) => if ↑i < m then p.2.2.2.2 i + a else p.2.2.2.2 i)

theorem Anderson4D.measurePreserving_r324TranslateLeftPhysical (m : ℕ) (a : T4) : MeasureTheory.MeasurePreserving (⇑(r324TranslateLeftPhysicalMeasurableEquiv m a)) (r324PhysicalMeasure m) (r324PhysicalMeasure m)

The left-copy translation preserves the genuine physical measure.

Translation multipliers of one configuration

theorem Anderson4D.renormalizedGreenSkeleton_add_const {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) (a : T4) : (renormalizedGreenSkeleton κ fun (i : Fin (m + 2)) => x i + a) = renormalizedGreenSkeleton κ x

A renormalized Green skeleton depends only on coordinate differences.

noncomputable def Anderson4D.SmoothCutoff.r324LeftPairModeContribution {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) (j : Fin {i ∈ κ.pairSupport | i < κ i}.card) : Z4

Signed contribution of one covariance pair to translation of the left copy.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324LeftModeSum {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) : Z4

Total signed covariance mode carried by the left physical copy.

Equations

• Anderson4D.SmoothCutoff.r324LeftModeSum κ q = ∑ j : Fin {i ∈ κ.pairSupport | i < κ i}.card, Anderson4D.SmoothCutoff.r324LeftPairModeContribution κ q j

theorem Anderson4D.SmoothCutoff.r324PairModeTerm_translateLeft (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) (j : Fin {i ∈ κ.pairSupport | i < κ i}.card) (a : T4) : ρ.r324PairModeTerm ε κ ((r324LeftInternalTranslateMeasurableEquiv m a) v) j (q j) = ρ.r324PairModeTerm ε κ v j (q j) * charT4 (r324LeftPairModeContribution κ q j) a

Translation multiplier of one enumerated covariance pair.

theorem Anderson4D.SmoothCutoff.prod_charT4_r324LeftPairModeContribution {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) (a : T4) : ∏ j : Fin {i ∈ κ.pairSupport | i < κ i}.card, charT4 (r324LeftPairModeContribution κ q j) a = charT4 (r324LeftModeSum κ q) a

Product characters turn the sum of signed pair contributions into one character.

theorem Anderson4D.SmoothCutoff.r324CovarianceFourierConfigurationTerm_translateLeft (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) (a : T4) : ρ.r324CovarianceFourierConfigurationTerm ε κ ((r324LeftInternalTranslateMeasurableEquiv m a) v) q = ρ.r324CovarianceFourierConfigurationTerm ε κ v q * charT4 (r324LeftModeSum κ q) a

Translation multiplier of the entire covariance configuration.

Conservation in the integrated configuration

theorem Anderson4D.SmoothCutoff.momentFourierPhase_translateLeft (α β : Z4) (x y z w a : T4) : momentFourierPhase α β (x + a) (y + a) z w = momentFourierPhase α β x y z w * charT4 (α + β) a

theorem Anderson4D.SmoothCutoff.assemble_r324LeftInternalTranslate_left {m : ℕ} (x y a : T4) (v : Fin (2 * m) → T4) : (assemble (x + a) (y + a) fun (i : Fin m) => (r324LeftInternalTranslateMeasurableEquiv m a) v (leftMomentIndex i)) = fun (j : Fin (m + 2)) => assemble x y (fun (i : Fin m) => v (leftMomentIndex i)) j + a

theorem Anderson4D.SmoothCutoff.r324LeftInternalTranslate_right {m : ℕ} (a : T4) (v : Fin (2 * m) → T4) : (fun (i : Fin m) => (r324LeftInternalTranslateMeasurableEquiv m a) v (rightMomentIndex i)) = fun (i : Fin m) => v (rightMomentIndex i)

theorem Anderson4D.SmoothCutoff.r324Flatten_fullPairingFourierIntegrand_translateLeft (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) (a : T4) (p : R324PhysicalPoint m) : r324Flatten (ρ.r324FullPairingFourierIntegrand ε α β κ q) ((r324TranslateLeftPhysicalMeasurableEquiv m a) p) = r324Flatten (ρ.r324FullPairingFourierIntegrand ε α β κ q) p * charT4 (α + β + r324LeftModeSum (↑κ) q) a

A translated configuration integrand picks up exactly the character of the external mode plus the signed left-copy covariance mode.

theorem Anderson4D.SmoothCutoff.r324FullPairingFourierIntegral_eq_mul_character (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) (a : T4) : ρ.r324FullPairingFourierIntegral ε α β κ q = ρ.r324FullPairingFourierIntegral ε α β κ q * charT4 (α + β + r324LeftModeSum (↑κ) q) a

Haar invariance makes a configuration integral an eigenvector of every left-copy translation.

theorem Anderson4D.SmoothCutoff.exists_charT4_ne_one_of_ne_zero (k : Z4) (hk : k ≠ 0) : ∃ (a : T4), charT4 k a ≠ 1

Every nontrivial torus frequency has a point where its character is not one.

theorem Anderson4D.SmoothCutoff.r324FullPairingFourierIntegral_eq_zero_of_frequency_ne (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) (hfrequency : α + β + r324LeftModeSum (↑κ) q ≠ 0) : ρ.r324FullPairingFourierIntegral ε α β κ q = 0

A Fourier configuration violating frequency conservation has zero physical integral.

theorem Anderson4D.SmoothCutoff.r324LeftModeSum_eq_neg_external_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) (hne : ρ.r324FullPairingFourierIntegral ε α β κ q ≠ 0) : r324LeftModeSum (↑κ) q = -(α + β)

Therefore every nonzero integrated configuration satisfies the exact left-copy conservation law.