Direct incoming Fourier evaluation at the initial R-324 root

At the all-Green initial state, production slot zero is the translated incoming Green leg. Every other factor in the slot-zero-erased residual is independent of the incoming endpoint. Hence its one-variable Fourier integral is exactly the paper second-order mode decay times the phased slot-zero-erased density.

This file deliberately proves only the pointwise one-variable identity. It does not change product coordinates or invoke a global Fubini theorem.

Incoming-endpoint independence away from slot zero

Initial slot-zero Fourier evaluation

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_charT4_mul_initialResidual_mul_const_eq_incomingPhased (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (coefficient : ℂ) (k : Z4) (y : T4) (v : (initial ρ lam ε pairing).SurvivingCoordinate → T4) : ∫ (x : T4), charT4 k x * (↑((initial ρ lam ε pairing).residualIntegrand ρ ε x y ((initial ρ lam ε pairing).reconstruct v)) * coefficient) ∂paperMeasure = (initial ρ lam ε pairing).incomingPhasedResidualDensity (↑(paperSecondOrderModeDecay k) * coefficient) k ρ ε 0 y v

Exact direct-incoming Fourier evaluation at the all-Green initial residual. The arbitrary scalar coefficient contains every factor that is constant in the incoming endpoint; in root applications it carries the other three endpoint characters, the opposite residual, and the cross factor.