The direct/exceptional half in paper Step 4(A) #
This file contains only the literal outgoing ordinary-J operation needed
by a DE x DD endpoint pattern. The proper prefix is removed while the
integrand is signed; the retained terminal is then evaluated by the paper's
ordinary primitive defect. Its norm is taken only after that evaluation.
No route mass, auxiliary tree sum, or uniform eps ^ (-8) estimate is
introduced here.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.incomingErasedHeadOuterFactor_eq_terminalPost_endpointErasedSignedChain
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix rho lam eps pairing}
(data : res.R324PaperOutgoingEndpointTerminal)
(hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0)
(hactive : data.terminalPost.state.active.Nonempty)
(x y : T4)
(v : data.terminalPost.SurvivingCoordinate → T4)
:
data.endpoint.stop.incomingErasedHeadOuterFactor data.terminalData.terminal [] ⋯ rho eps x y v = data.terminalPost.endpointErasedSignedChain hactive x y (data.terminalPost.reconstruct v)
Generic retained-terminal chain identity. It is the literal last algebraic step of paper Step 4(A), valid independently of which endpoint case selected the outgoing terminal.
def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.geometry
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
The structural DE route is exactly the canonical retained-terminal
geometry consumed by the signed outgoing endpoint theorem.
Instances For
@[simp]
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.geometry_paperOutgoingTerminal
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.stopBudgetCertificate
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
The synchronized budget retained on the literal pre-terminal state is a certificate for the terminal context appearing in the signed outgoing defect.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.outgoingProp41
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(H : Fin (2 * residualBlockOrder data.outgoing.terminalData.terminal.2 - 1) → T4 → ℝ)
:
IsAdmissiblePrimitiveInput (residualBlockOrder data.outgoing.terminalData.terminal.2) H →
MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4
(primitiveKernelInsertedDiff rho lam eps (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ H
providers.supportConstant C
Proposition 4.1 specialized to the retained outgoing terminal.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.endpoint_multiplier_eq_one
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(mode : Z4)
:
The direct prefix of a literal DE half contributes no exceptional
incoming multiplier.
def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.postBudgetScale
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
The complete-budget scale obtained by consuming the retained outgoing terminal. This is the literal Step-4 budget update, not a new estimate.
Equations
- data.postBudgetScale = data.endpoint.stop.budgetUpdatedEdgeScale data.terminalData.terminal [] ⋯ data.stopBudgetScale C lam K
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.postBudgetReachable
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A data.outgoing.terminalPost.state data.postBudgetScale
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.postBudgetCertificate
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.postBudget_activeProduct_eq_route
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.postBudgetScale edge = ∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.route.terminalScale edge
The canonical post-terminal update and the completed route have the same active scale product because both are complete reachable histories on the same final state.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.postBudgetScale_zero_eq_stopBudget
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.outgoingBudgetCore_le_postBudget_outgoingScale
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
data.stopBudgetScale
(r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.stopBudgetScale * (C * lam) ^ (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) * K ≤ data.postBudgetScale (data.outgoing.terminalPost.terminalOutgoingEdgeSlot ⋯)
The outgoing ordinary-J local block charge is exactly one boundary
slot of the post-terminal complete budget, up to the already assumed
A >= 1.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.boundaryCore_mul_endpointErasedScale_le_routeActiveProduct
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
:
data.stopBudgetScale 0 * (data.stopBudgetScale
(r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.stopBudgetScale * (C * lam) ^ (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) * K) * data.outgoing.terminalPost.endpointErasedScaleProduct ⋯ data.postBudgetScale ≤ ∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.route.terminalScale edge
The direct incoming budget, the retained outgoing local charge, and the erased post-terminal chain occupy precisely the three factors of the completed active scale product.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_terminalSplitOuter_le_postBudgetMajorant
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(x : T4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
(hne :
∀ edge ∈ data.outgoing.terminalPost.endpointErasedActiveEdgeSlots ⋯,
data.outgoing.terminalPost.edgeDisplacement 0 0 (data.outgoing.terminalPost.reconstruct v) edge ≠ 0)
:
‖data.outgoing.terminalSplitOuter coefficient incomingMode x v‖ ≤ ‖coefficient v‖ * (data.outgoing.terminalPost.endpointErasedScaleProduct ⋯ data.postBudgetScale * data.outgoing.terminalPost.endpointErasedInvSqChainProduct ⋯ v)
After the signed retained-terminal identity, its outer factor is the literal endpoint-erased post chain.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_integral_outgoingEndpointDefectDensity_le_inserted
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(x : T4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
‖∫ (first : T4), data.outgoing.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure‖ ≤ data.stopBudgetScale
(r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * invSqKerMass * paperSecondOrderModeDecay outgoingMode * (2 * r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.stopBudgetScale * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ∫ (gap : T4), primitiveInsertedMajorant C lam eps providers.supportConstant
(residualBlockOrder data.outgoing.terminalData.terminal.2) gap ∂paperMeasure)) * ‖data.outgoing.terminalSplitOuter coefficient incomingMode x v‖
Literal numerical exit of the exceptional outgoing endpoint. The ordinary primitive defect is bounded by Proposition 4.1 and converted to the inserted-kernel currency with exactly one endpoint sacrifice.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_integral_outgoingEndpointDefectDensity_le_budgeted
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(x : T4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
‖∫ (first : T4), data.outgoing.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure‖ ≤ data.stopBudgetScale
(r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * invSqKerMass * paperSecondOrderModeDecay outgoingMode * (r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.stopBudgetScale * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ((C * lam) ^ (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) * K))) * ‖data.outgoing.terminalSplitOuter coefficient incomingMode x v‖
Pay the one inserted primitive integral by the existing local block constant. The literal exceptional endpoint sacrifice is not enlarged.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.directIncomingEndpointCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
The direct incoming Green leg after its exact Fourier integration.
The phase is already carried by terminalSplitOuter; hence the only new
scalar is the literal second-order Fourier multiplier.
Equations
- data.directIncomingEndpointCoefficient coefficient v = ↑(Anderson4D.paperSecondOrderModeDecay incomingMode) * coefficient v
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_directIncomingEndpointCoefficient
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
‖data.directIncomingEndpointCoefficient coefficient v‖ = paperSecondOrderModeDecay incomingMode * ‖coefficient v‖
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.endpointDensity
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(x : T4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
:
One complete literal DE half after the direct incoming Fourier
operation and the signed retained outgoing-terminal operation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfDirectExceptionalRoute.norm_endpointDensity_le
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(data : R324PaperHalfDirectExceptionalRoute providers)
(coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(outgoingMode : Z4)
(x : T4)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4)
(hne :
∀ edge ∈ data.outgoing.terminalPost.endpointErasedActiveEdgeSlots ⋯,
data.outgoing.terminalPost.edgeDisplacement 0 0 (data.outgoing.terminalPost.reconstruct v) edge ≠ 0)
:
‖data.endpointDensity coefficient outgoingMode x v‖ ≤ paperSecondOrderModeDecay incomingMode * paperSecondOrderModeDecay outgoingMode * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.directFourier * SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice) * ((∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.route.terminalScale edge) * invSqKerMass) * data.outgoing.terminalPost.endpointErasedInvSqChainProduct ⋯ v * ‖coefficient v‖
Pointwise Step 4(A) estimate for the literal direct/exceptional half.
The norm is taken only after both endpoint operations. The synchronized
ordinary prefix keeps stopBudgetScale 0 = A; its assumed A >= 1 pays
the otherwise harmless direct incoming boundary slot.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.directExceptionalDirectDirectTerminalData
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{leftMode rightMode : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP leftMode}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
:
R324TwoHalfTerminalData rho lam eps kappaP kappaM
The literal terminal carrier of the DE x DD row of the paper's
endpoint table.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.terminal_directExceptional_directDirect_eq
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{leftMode rightMode : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP leftMode}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(hleftFirst : ⟨0, ⋯⟩ ∈ finalActive kappaP)
(hleftOutgoing : Fin.last m ∈ extractedRightEdges kappaP)
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(hrightFirst : ⟨0, ⋯⟩ ∈ finalActive kappaM)
(hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
:
{ left := R324PaperHalfEndpointRoute.directExceptional hleftFirst hleftOutgoing leftDE,
right := R324PaperHalfEndpointRoute.directDirect hrightFirst hrightOutgoing rightDD }.terminal = directExceptionalDirectDirectTerminalData leftDE rightDD
The common completed-route terminal does not forget either concrete
carrier used by the signed DE x DD splice.
@[simp]
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.cases_directExceptional_directDirect
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{leftMode rightMode : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP leftMode}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(hleftFirst : ⟨0, ⋯⟩ ∈ finalActive kappaP)
(hleftOutgoing : Fin.last m ∈ extractedRightEdges kappaP)
(leftDE : R324PaperHalfDirectExceptionalRoute leftProviders)
(hrightFirst : ⟨0, ⋯⟩ ∈ finalActive kappaM)
(hrightOutgoing : Fin.last m ∉ extractedRightEdges kappaM)
(rightDD : R324PaperHalfDirectDirectRoute rightProviders)
:
{ left := R324PaperHalfEndpointRoute.directExceptional hleftFirst hleftOutgoing leftDE,
right := R324PaperHalfEndpointRoute.directDirect hrightFirst hrightOutgoing rightDD }.cases = ![SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.insertedSacrifice, SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.directFourier]
The concrete cost pattern is exactly direct, inserted, direct, direct; no uniform eps ^ (-8) charge is inserted.