Uniform interface for the four literal one-half endpoint branches

This file packages the four already completed signed endpoint calculations without expanding the two-half argument into sixteen cases. The carrier is kept branch-literal, together with its equality to the common completed route. A direct outgoing endpoint contributes mass 1; a retained exceptional outgoing endpoint contributes the one genuine invSqKerMass. No uniform mass or endpoint sacrifice is inserted here.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324PaperHalfOutgoingEndpointMass : SmoothCutoff.R324EndpointReductionCase → ℝ

The exact spatial mass produced by the outgoing endpoint operation.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.r324PaperHalfOutgoingEndpointMass Anderson4D.SmoothCutoff.R324EndpointReductionCase.directFourier = 1
• Anderson4D.R324WithinHalfResidualPrefix.r324PaperHalfOutgoingEndpointMass Anderson4D.SmoothCutoff.R324EndpointReductionCase.insertedSacrifice = Anderson4D.invSqKerMass

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324PaperHalfOutgoingEndpointMass_direct : r324PaperHalfOutgoingEndpointMass SmoothCutoff.R324EndpointReductionCase.directFourier = 1

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324PaperHalfOutgoingEndpointMass_inserted : r324PaperHalfOutgoingEndpointMass SmoothCutoff.R324EndpointReductionCase.insertedSacrifice = invSqKerMass

theorem Anderson4D.R324WithinHalfResidualPrefix.r324PaperHalfOutgoingEndpointMass_nonneg (c : SmoothCutoff.R324EndpointReductionCase) : 0 ≤ r324PaperHalfOutgoingEndpointMass c

structure Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (route : R324PaperHalfCompletedRoute pairing incomingMode) : Type

Common pointwise output of any one-half endpoint branch. The density is coefficient-parametric because the second half supplies the untouched cross primitive factor only after both signed endpoint computations have been chosen.

• carrier : R324WithinHalfResidualPrefix rho lam eps pairing
• route_final : route.final = self.carrier
• carrier_remaining : self.carrier.remaining = []
• carrier_processed : self.carrier.state.processed = r322AnalyticSchedule pairing
• active : self.carrier.state.active.Nonempty
• density : ((self.carrier.SurvivingCoordinate → T4) → ℂ) → Z4 → (self.carrier.SurvivingCoordinate → T4) → ℂ
• norm_density_le (coefficient : (self.carrier.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (v : self.carrier.SurvivingCoordinate → T4) : (∀ edge ∈ self.carrier.endpointErasedActiveEdgeSlots ⋯, self.carrier.edgeDisplacement 0 0 (self.carrier.reconstruct v) edge ≠ 0) → ‖self.density coefficient outgoingMode v‖ ≤ paperSecondOrderModeDecay incomingMode * paperSecondOrderModeDecay outgoingMode * route.endpointSacrifice * ((∏ edge ∈ self.carrier.activeEdgeSlots, route.terminalScale edge) * r324PaperHalfOutgoingEndpointMass (route.cases 1)) * self.carrier.endpointErasedInvSqChainProduct ⋯ v * ‖coefficient v‖

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ofDirectDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (data : R324PaperHalfDirectDirectRoute providers) : R324PaperHalfEndpointUniformBound data.route

The direct/direct calculation in the common one-half interface.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ofDirectExceptional {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfDirectExceptionalRoute providers) : R324PaperHalfEndpointUniformBound data.route

The direct/exceptional calculation in the common one-half interface.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ofExceptionalDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (data : R324PaperHalfExceptionalDirectRoute providers) : R324PaperHalfEndpointUniformBound data.route

The exceptional/direct calculation in the common one-half interface.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ofExceptionalExceptional {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (hsingles : pairing.singles.Nonempty) (data : R324PaperHalfExceptionalExceptionalRoute providers) : R324PaperHalfEndpointUniformBound data.route

The exceptional/exceptional calculation in the common one-half interface. The surviving-single hypothesis supplies exactly the two geometric facts required by the retained outgoing endpoint.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.exists_endpointUniformBound_of_singles {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (route : R324PaperHalfEndpointRoute providers) (hsingles : pairing.singles.Nonempty) : Nonempty (R324PaperHalfEndpointUniformBound route.completedRoute)

Exhaustive one-half producer. The four signed calculations are packaged once here; later two-half code consumes two uniform packages and does not repeat a sixteen-way case split.