Per-mode majorant for the marked R-324 residual block

The marker-preserving residual decomposition leaves exactly one projected cross covariance in one genuine residual block. This file expands that projected factor into its high Fourier modes while every other covariance in the block remains the complete physical etaEpsT4 factor.

The resulting pointwise estimate extracts the paper's central eighthOrderFrequencyDecay (ε ^ 2 * L) payoff. It is deliberately a per-mode comparison with the covariance at the marked edge deleted. Standard Proposition 4.1 estimates the complete primitive covariance sum; it does not estimate this deleted-edge integrand. Consequently this file does not claim a projected primitive-kernel bound.

Exact projected-mode expansion

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

Product of all complete physical covariances in the marked block except for the unique selected cross edge.

Equations

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

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

One high Fourier mode at the marked cross edge, multiplied by all unselected complete covariance factors in its genuine residual block.

Equations

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

theorem Anderson4D.SmoothCutoff.pairingCovarianceProductOn_markedBlock_eq_selected_mul_unselected (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ↑(pairingCovarianceProductOn ρ ε (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) v) = ↑(ρ.etaEpsT4 ε (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected))) * ρ.r324MarkedResidualBlockUnselectedCovarianceProduct ε κp κm π selected v

The ordinary complete covariance factor on the same physical block is the selected full etaEpsT4 covariance times the deleted-edge product. Together with pairingCovarianceProductOn_eq_residualPrimitiveBlock, this identifies the precise input controlled by Proposition 4.1.

theorem Anderson4D.SmoothCutoff.summable_r324MarkedResidualBlockModeTerm (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : Summable (ρ.r324MarkedResidualBlockModeTerm ε L κp κm π selected v)

theorem Anderson4D.SmoothCutoff.r324MarkedPairingCovarianceProductOn_markedBlock_eq_tsum_modes (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ρ.r324MarkedPairingCovarianceProductOn ε L (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324MarkedResidualBlock κp κm π selected) v = ∑' (k : Z4), ρ.r324MarkedResidualBlockModeTerm ε L κp κm π selected v k

The actual marked-block covariance product is the absolutely convergent sum of the one-mode marked terms. No unselected covariance is Fourier-expanded here.

The central frequency payoff

theorem Anderson4D.SmoothCutoff.exists_norm_r324HighCovarianceModeTerm_le_decay (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε L : ℝ} {z : T4} {k : Z4}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → ‖ρ.r324HighCovarianceModeTerm ε L z k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L)

The high-mode indicator itself satisfies the same uniform central frequency bound, including modes outside the retained set (where it vanishes).

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

The product of norms of the complete, unselected physical covariances.

Equations

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

theorem Anderson4D.SmoothCutoff.r324MarkedResidualBlockUnselectedCovarianceMass_nonneg (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : 0 ≤ ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v

theorem Anderson4D.SmoothCutoff.norm_r324MarkedResidualBlockUnselectedCovarianceProduct (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) : ‖ρ.r324MarkedResidualBlockUnselectedCovarianceProduct ε κp κm π selected v‖ = ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v

theorem Anderson4D.SmoothCutoff.exists_norm_r324MarkedResidualBlockModeTerm_le (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {m : ℕ} {ε L : ℝ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {v : Fin (2 * m) → T4} {k : Z4}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → ‖ρ.r324MarkedResidualBlockModeTerm ε L κp κm π selected v k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L) * ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v

Honest per-mode marked-block comparison.

The selected projected covariance supplies the central decay. The remaining factor is exactly the product of norms of all unselected, unexpanded etaEpsT4 covariances in the same physical block.

theorem Anderson4D.SmoothCutoff.exists_norm_mul_r324MarkedResidualBlockModeTerm_le (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {m : ℕ} {ε L : ℝ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {selected : R324ResidualCovarianceSlot κp} {v : Fin (2 * m) → T4} {k : Z4} {amplitude : ℂ}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → ‖amplitude * ρ.r324MarkedResidualBlockModeTerm ε L κp κm π selected v k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L) * (‖amplitude‖ * ρ.r324MarkedResidualBlockUnselectedCovarianceMass ε κp κm π selected v)

The same bound after multiplying by an arbitrary genuine Green-chain or endpoint amplitude. This is the pointwise consumer needed before integrating a marked primitive coordinate.