The exceptional/direct half after both endpoint operations

This is the literal paper Step 4(A) ED half. The incoming exceptional head is collapsed exactly, its signed coefficient is transported through the remaining schedule, and the direct outgoing Fourier operation is then performed on the completed carrier. Norms are taken only after these two operations. No auxiliary mass or summation is introduced.

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

Exact scalar left after the exceptional incoming collapse and the signed transport of its remaining suffix. The first displayed decay is the root Fourier decay; incomingExceptionalHeadCollapseFactor contains the second decay and the primitive defect.

Equations

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

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

Literal ED density after the direct outgoing Fourier operation.

Equations

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

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

The already-existing complete after-head budget pays the transported incoming exceptional coefficient.

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

A direct outgoing boundary retains the base scale A.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalDirectRoute.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 : R324PaperHalfExceptionalDirectRoute 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

Slot zero and the erased interior scale product are contained in the full completed active scale product.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalDirectRoute.norm_endpointDensity_le_directCore {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalDirectRoute 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.endpointDensity 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 bound before the harmless case-ledger enlargement for the incoming inserted sacrifice.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalDirectRoute.norm_endpointDensity_le {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalDirectRoute 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.endpointDensity hactive coefficient outgoingMode v‖ ≤ (paperSecondOrderModeDecay incomingMode * paperSecondOrderModeDecay outgoingMode * SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ∏ edge ∈ data.transport.final.activeEdgeSlots, data.route.terminalScale edge) * data.transport.final.endpointErasedInvSqChainProduct hactive v * ‖coefficient v‖

Literal ED case-ledger estimate. The inserted factor records the already completed incoming exceptional operation; it is introduced only after the signed density has been fully evaluated.