The direct/direct half after both endpoint Fourier operations

This is the literal paper Step 4(A) DD half. The alternating transport is kept signed to its terminal carrier; the two direct endpoint operations then contribute their exact second-order Fourier multipliers. Only after that exact expression has been formed is its norm bounded by the completed route scale product and the endpoint-erased inverse-square path.

No artificial inverse-square mass or new summation is introduced here.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectDirectRoute.directIncomingCoefficient {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectDirectRoute providers) (coefficient : (data.transport.final.SurvivingCoordinate → T4) → ℂ) (v : data.transport.final.SurvivingCoordinate → T4) : ℂ

The exact direct incoming Fourier scalar, attached only after the signed alternating transport has reached its final carrier.

Equations

• data.directIncomingCoefficient coefficient v = data.transport.multiplier incomingMode * (↑(Anderson4D.paperSecondOrderModeDecay incomingMode) * coefficient v)

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectDirectRoute.transportEndpointDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectDirectRoute providers) (hactive : data.transport.final.state.active.Nonempty) (coefficient : (data.transport.final.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (v : data.transport.final.SurvivingCoordinate → T4) : ℂ

Complete literal DD half after both direct endpoint Fourier operations.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectDirectRoute.norm_directIncomingCoefficient_le {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectDirectRoute providers) (coefficient : (data.transport.final.SurvivingCoordinate → T4) → ℂ) (v : data.transport.final.SurvivingCoordinate → T4) : ‖data.directIncomingCoefficient coefficient v‖ ≤ data.route.terminalScale 0 * paperSecondOrderModeDecay incomingMode * ‖coefficient v‖

The transported multiplier, together with the direct incoming Fourier decay, is paid by terminal slot zero.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectDirectRoute.terminalScale_outgoing_eq_base {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectDirectRoute providers) (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (hactive : data.transport.final.state.active.Nonempty) : data.route.terminalScale (data.transport.final.terminalOutgoingEdgeSlot hactive) = A

In a direct outgoing branch the final boundary scale is still the initial base A.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectDirectRoute.terminalScale_zero_mul_endpointErasedScaleProduct_le_activeProduct {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectDirectRoute providers) (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (hactive : data.transport.final.state.active.Nonempty) : data.route.terminalScale 0 * data.transport.final.endpointErasedScaleProduct hactive data.route.terminalScale ≤ ∏ edge ∈ data.transport.final.activeEdgeSlots, data.route.terminalScale edge

Terminal slot zero and the endpoint-erased scale product are dominated by the complete active scale product. The direct incoming multiplier has already been paid by slot zero in norm_directIncomingCoefficient_le.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectDirectRoute.norm_transportEndpointDensity_le {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectDirectRoute providers) (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (hactive : data.transport.final.state.active.Nonempty) (coefficient : (data.transport.final.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (v : data.transport.final.SurvivingCoordinate → T4) (hne : ∀ edge ∈ data.transport.final.endpointErasedActiveEdgeSlots hactive, data.transport.final.edgeDisplacement 0 0 (data.transport.final.reconstruct v) edge ≠ 0) : ‖data.transportEndpointDensity hactive coefficient outgoingMode v‖ ≤ (paperSecondOrderModeDecay incomingMode * paperSecondOrderModeDecay outgoingMode * ∏ edge ∈ data.transport.final.activeEdgeSlots, data.route.terminalScale edge) * data.transport.final.endpointErasedInvSqChainProduct hactive v * ‖coefficient v‖

Pointwise paper Step 4(A) estimate for a literal DD half. Both direct Fourier multipliers remain explicit; the spatial part is exactly the completed route's active scale product times its endpoint-erased path.