Incoming Fourier integration before an exceptional R-324 collapse

At an exceptional incoming step, the incoming external Green edge must be Fourier-integrated before the block is absorbed into slot zero. This file proves that exact local identity for a fixed translated block tuple. The primitive-pairing sum stays grouped and no block-coordinate integral is reordered.

The later global bridge must still transport the original refined physical integral to this reachable pre-step state and justify the corresponding joint Fubini exchange.

noncomputable def Anderson4D.R324WithinHalfStepContext.incomingErasedTranslatedRawLocalCore {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ℂ

The translated raw local factor after removing only its incoming predecessor edge. The outgoing signed difference and the complete primitive covariance sum remain literal.

Equations

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

theorem Anderson4D.R324WithinHalfStepContext.rawLocalIntegrand_translated_eq_incomingGreen_mul_core {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (hincoming : ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) = greenFn) (x a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ↑(ctx.rawLocalIntegrand ρ ε (x - a) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - a) = ↑(greenFn (x - t ⟨0, ⋯⟩)) * ctx.incomingErasedTranslatedRawLocalCore ρ ε a t

Pointwise separation of the untouched incoming Green edge from the translated raw local density.

theorem Anderson4D.R324WithinHalfStepContext.integral_char_mul_rawLocal_translated_eq {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (hincoming : ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) = greenFn) (k : Z4) (a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) (outer : ℂ) : ∫ (x : T4), charT4 k x * (↑(ctx.rawLocalIntegrand ρ ε (x - a) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - a) * outer) ∂paperMeasure = translatedGreenMode k (t ⟨0, ⋯⟩) * ctx.incomingErasedTranslatedRawLocalCore ρ ε a t * outer

Exact local pre-collapse Fourier identity. The incoming external variable is integrated while its edge is still the free Green kernel. Every other local factor, including the signed primitive sum, is a literal constant with respect to that variable.

theorem Anderson4D.R324WithinHalfStepContext.norm_integral_char_mul_rawLocal_translated_eq {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (hincoming : ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) = greenFn) (k : Z4) (a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) (outer : ℂ) : ‖∫ (x : T4), charT4 k x * (↑(ctx.rawLocalIntegrand ρ ε (x - a) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - a) * outer) ∂paperMeasure‖ = paperSecondOrderModeDecay k * ‖ctx.incomingErasedTranslatedRawLocalCore ρ ε a t‖ * ‖outer‖

Norm form of the local incoming Fourier identity.

theorem Anderson4D.R324IncomingExceptionalStop.integral_char_mul_rawLocal_translated_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) (hm : 0 < m) (k : Z4) (a : T4) (t : Fin (2 * residualBlockOrder stop.ctx.step.2) → T4) (outer : ℂ) : ∫ (x : T4), charT4 k x * (↑(stop.ctx.rawLocalIntegrand ρ ε (x - a) fun (j : Fin (2 * residualBlockOrder stop.ctx.step.2)) => t j - a) * outer) ∂paperMeasure = translatedGreenMode k (t ⟨0, ⋯⟩) * stop.ctx.incomingErasedTranslatedRawLocalCore ρ ε a t * outer

Consumer form for the genuine exceptional stop constructed from the analytic schedule.

theorem Anderson4D.R324IncomingExceptionalStop.norm_integral_char_mul_rawLocal_translated_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) (hm : 0 < m) (k : Z4) (a : T4) (t : Fin (2 * residualBlockOrder stop.ctx.step.2) → T4) (outer : ℂ) : ‖∫ (x : T4), charT4 k x * (↑(stop.ctx.rawLocalIntegrand ρ ε (x - a) fun (j : Fin (2 * residualBlockOrder stop.ctx.step.2)) => t j - a) * outer) ∂paperMeasure‖ = paperSecondOrderModeDecay k * ‖stop.ctx.incomingErasedTranslatedRawLocalCore ρ ε a t‖ * ‖outer‖

The genuine exceptional stop gains exactly one second-order incoming Green multiplier before its slot-zero collapse.