The pairwise spatial orthogonality behind the double-sum formula for the moving-cutoff corrector energy.

theorem AVenhance.Infra.Section3.MovingEnergyReduction.xiMK_mem_support_window {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) (hξ : I.xiMK m k t ≠ 0) : (t - ↑k * tau β I.Λ m) / tau β I.Λ m ∈ Set.Icc (-(5 / 4)) (5 / 4)

theorem AVenhance.Infra.Section3.MovingEnergyReduction.odd_mode_distance_le_two_of_xi_overlap {β : ℝ} (I : Ingredients β) {m : ℕ} {k l : ℤ} (t : ℝ) (hξk : I.xiMK m k t ≠ 0) (hξl : I.xiMK m l t ≠ 0) : |k - l| ≤ 2

theorem AVenhance.Infra.Section3.MovingEnergyReduction.chiMK_horizontal_other_component {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) : (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section3.MovingEnergyReduction.chiMK_vertical_other_component {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) : (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section3.MovingEnergyReduction.chiMKGrad_horizontal {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) (hε : epsilon β I.Λ m ≠ 0) (x : Homogenization.Vec 2) : gradMatrix (I.chiMK κ m k t) x = (4 * Real.pi ^ 2 * a β I.Λ m * I.corrTime κ m k t * Real.sin (2 * Real.pi * x 0 / epsilon β I.Λ m)) • Matrix.single 0 1 1

theorem AVenhance.Infra.Section3.MovingEnergyReduction.chiMKGrad_vertical {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) (hε : epsilon β I.Λ m ≠ 0) (x : Homogenization.Vec 2) : gradMatrix (I.chiMK κ m k t) x = (-(4 * Real.pi ^ 2 * a β I.Λ m * I.corrTime κ m k t) * Real.sin (2 * Real.pi * x 1 / epsilon β I.Λ m)) • Matrix.single 1 0 1

theorem AVenhance.Infra.Section3.xiMK_odd_overlap_distance {β : ℝ} (I : Ingredients β) {m : ℕ} {k l : ℤ} (hk : Odd k) (hl : Odd l) (t : ℝ) (hξk : I.xiMK m k t ≠ 0) (hξl : I.xiMK m l t ≠ 0) (hne : k ≠ l) : |k - l| = 2

If two distinct odd transition windows are simultaneously nonzero, their indices differ by exactly two.

theorem AVenhance.Infra.Section3.chiMK_grad_cross_eq_zero_of_odd_overlap {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) {k l : ℤ} (hk : Odd k) (hl : Odd l) (hne : k ≠ l) (t : ℝ) (hξk : I.xiMK m k t ≠ 0) (hξl : I.xiMK m l t ≠ 0) (x y : Homogenization.Vec 2) : (gradMatrix (I.chiMK κ m k t) x).transpose * gradMatrix (I.chiMK κ m l t) y = 0

Adjacent odd shear correctors have orthogonal gradient tensors, pointwise in both spatial arguments.

theorem AVenhance.Infra.Section3.movingEnergy_gram_double_sum_reduces {β : ℝ} (I : Ingredients β) {m : ℕ} (κ t : ℝ) (S : Finset { k : ℤ // Odd k }) (x : Homogenization.Vec 2) (hS : ∀ k ∈ S, I.xiMK m (↑k) t ≠ 0) : ∑ k ∈ S, ∑ l ∈ S, (I.xiMK m (↑k) t * I.xiMK m (↑l) t) • ((gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑l) t) x) = ∑ k ∈ S, I.xiMK m (↑k) t ^ 2 • ((gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑k) t) x)

The moving-cutoff double sum of gradient Gram matrices has only its diagonal terms. This is the exact reduction of the quadratic part of the source's E_m formula; it uses support overlap before discarding cross terms.

theorem AVenhance.Infra.Section3.movingEnergy_double_sum_reduces {β : ℝ} (I : Ingredients β) {m : ℕ} (κ t : ℝ) (S : Finset { k : ℤ // Odd k }) (x : Homogenization.Vec 2) (hS : ∀ k ∈ S, I.xiMK m (↑k) t ≠ 0) (hpartition : ∑ k ∈ S, I.xiMK m (↑k) t = 1) : ∑ k ∈ S, ∑ l ∈ S, (I.xiMK m (↑k) t * I.xiMK m (↑l) t) • (κ • 1 + (gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑l) t) x) = κ • 1 + ∑ k ∈ S, I.xiMK m (↑k) t ^ 2 • ((gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑k) t) x)

The complete double-sum energy keeps the full molecular baseline. The cutoff partition enters as (∑ ξ_k)^2 = 1; only the gradient correction is reduced to the diagonal. This is the correction to the printed Σ ξ_k² I baseline used in the source.

theorem AVenhance.Infra.Section3.xiMK_odd_partition_finset {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : have S := ⋯.toFinset; ∑ k ∈ S, I.xiMK m (↑k) t = 1

The finite support selected by the moving cutoffs carries the full partition of unity. This is the finite-sum form needed to apply the double-sum reduction at a fixed time.

theorem AVenhance.Infra.Section3.movingEnergy_odd_cutoff_double_sum_reduces {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (x : Homogenization.Vec 2) : have S := ⋯.toFinset; ∑ k ∈ S, ∑ l ∈ S, (I.xiMK m (↑k) t * I.xiMK m (↑l) t) • (κ • 1 + (gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑l) t) x) = κ • 1 + ∑ k ∈ S, I.xiMK m (↑k) t ^ 2 • ((gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑k) t) x)

The source's full odd-mode double sum reduces on the actual finite cutoff support. This specializes the overlap cancellation and molecular partition identity to the E_m sum at a fixed time.