Outgoing Fourier integration before the terminal shortcut collapse

For an arbitrary certified within-half step whose outgoing named edge is still greenFn, this file removes that edge from the translated raw local density and Fourier-integrates the resulting Green difference exactly. The predecessor edge, internal primitive chain, and complete primitive covariance sum remain grouped in one scalar.

The consumer at the end specializes this identity to the retained head of R324ShortcutStopTraceAssembly; its outgoing-Green hypothesis follows from reachability. Every result here is for one fixed block tuple and one fixed outer factor. No block-coordinate Fubini exchange, residual-sum interchange, or global R-324 closure is asserted.

def Anderson4D.R324WithinHalfStepContext.outgoingBlockFirst {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : T4

The first point of the translated primitive block.

Equations

• ctx.outgoingBlockFirst t = t ⟨0, ⋯⟩

def Anderson4D.R324WithinHalfStepContext.outgoingBlockLast {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : T4

The last point of the translated primitive block.

Equations

• ctx.outgoingBlockLast t = t (Anderson4D.primitiveLast (Anderson4D.residualBlockOrder ctx.step.2) ⋯)

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

The translated raw local density with only the outgoing edge removed. It retains the predecessor edge, primitive chain, and the full finite sum over primitive covariance pairings.

Equations

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

theorem Anderson4D.R324WithinHalfStepContext.rawLocalIntegrand_translated_eq_outgoingCore_mul_greenDifference {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (x y : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - y) = ctx.outgoingErasedTranslatedRawLocalCore ρ ε x t * (↑(greenFn (ctx.outgoingBlockLast t - y)) - ↑(greenFn (ctx.outgoingBlockFirst t - y)))

Exact pointwise factorization retaining the signed outgoing Green difference.

theorem Anderson4D.R324WithinHalfStepContext.rawLocalIntegrand_translated_eq_outgoingCore_mul_endpointKernel {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (x y : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - y) = ctx.outgoingErasedTranslatedRawLocalCore ρ ε x t * r324OutgoingEndpointKernel (ctx.outgoingBlockLast t) (ctx.outgoingBlockFirst t) true y

Kernel form of the exact outgoing factorization.

theorem Anderson4D.R324WithinHalfStepContext.integral_char_mul_rawLocal_translated_eq_endpointCoefficient {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (ρ : SmoothCutoff) (ε : ℝ) (houtgoing : ctx.state.edges ctx.outgoingSlot = greenFn) (k : Z4) (x : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) (outer : ℂ) : ∫ (y : T4), charT4 k y * (↑(ctx.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - y) * outer) ∂paperMeasure = ctx.outgoingErasedTranslatedRawLocalCore ρ ε x t * r324EndpointCoefficient k (ctx.outgoingBlockLast t) (ctx.outgoingBlockFirst t) true * outer

Fixed-tuple outgoing Fourier identity. Only the external variable y is integrated; the block tuple and outer remain fixed.

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

The fixed-tuple identity gains the expected second-order outgoing multiplier, with the literal factor two from the endpoint difference.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.terminalContext {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324ShortcutStopTraceAssembly κ initialScale) : R324WithinHalfStepContext κ

The retained shortcut head as a generic within-half step context.

Equations

• data.terminalContext = data.trace.stopPrefix.headContext data.terminalData.terminal [] ⋯

theorem Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.terminalContext_outgoing_eq_greenFn {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324ShortcutStopTraceAssembly κ initialScale) : data.terminalContext.state.edges data.terminalContext.outgoingSlot = greenFn

Reachability automatically supplies the outgoing-Green hypothesis for the retained shortcut head.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.integral_char_mul_terminal_rawLocal_translated_eq {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324ShortcutStopTraceAssembly κ initialScale) (k : Z4) (x : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) (outer : ℂ) : ∫ (y : T4), charT4 k y * (↑(data.terminalContext.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder data.terminalContext.step.2)) => t j - y) * outer) ∂paperMeasure = data.terminalContext.outgoingErasedTranslatedRawLocalCore ρ ε x t * r324EndpointCoefficient k (data.terminalContext.outgoingBlockLast t) (data.terminalContext.outgoingBlockFirst t) true * outer

Shortcut-stop consumer of the generic fixed-tuple Fourier identity.