Fourier bridge for the marked residual physical core

The within-half phase of R-324 must be completed on the physical side, before the central-frequency covariance is expanded. This file records the exact next representation-order step for the resulting marked residual object:

• every unmarked residual block remains a complete physical covariance product;
• only the unique marked covariance is expanded into Fourier modes; and
• the signed left and right Green profiles remain outside that series.

No estimate for the original moment and no reduction-output hypothesis is used here.

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

One Fourier mode of the marked residual physical interior core.

All covariances outside the marked block, and every unselected covariance inside the marked block, remain complete physical etaEpsT4 factors.

Equations

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

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

The complete signed amplitude outside the one surviving Fourier mode. It retains every unselected covariance as a physical factor.

Equations

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

theorem Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalInteriorModeTerm_eq_highMode_mul_amplitude (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (v : Fin (2 * m) → T4) (k : Z4) : ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k = ρ.r324HighCovarianceModeTerm ε L (v (r324ResidualMarkedLowerEndpoint selected) - v (r324ResidualMarkedUpperEndpoint π selected)) k * ρ.r324MarkedResidualPhysicalOpenEdgeAmplitude ε κp κm π selected v

Exact consumer-facing factorization: the sole expanded factor is the high Fourier mode on the marked cross edge.

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

The one-marked-edge mode family is absolutely summable.

theorem Anderson4D.SmoothCutoff.r324MarkedResidualPhysicalInteriorCore_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) : ρ.r324MarkedResidualPhysicalInteriorCore ε L κp κm π selected v = ∑' (k : Z4), ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k

Exact representation-order bridge.

After the physical within-half collapse has produced the marked residual core, expanding only the surviving marked covariance gives this Z4 series. In particular, no covariance from an unmarked primitive block is Fourier-expanded or separated from its Green skeleton.

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

Absolute physical mass left after deleting only the selected projected edge. The unselected covariances are still grouped by their genuine physical primitive blocks.

Equations

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

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

theorem Anderson4D.SmoothCutoff.exists_norm_r324MarkedResidualPhysicalInteriorModeTerm_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 → ‖ρ.r324MarkedResidualPhysicalInteriorModeTerm ε L κp κm π selected v k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L) * ρ.r324MarkedResidualPhysicalComplementMass ε κp κm π selected v

The exact single-mode physical term carries the paper's central eighth-order decay. Crucially, the remaining factor is the complete physical complement mass, not a product of absolute Fourier coefficient sums.