Structural one-half endpoint routes for paper Step 4(A)

The signed endpoint identities live in R324PaperEndpointTwoHalfSplice and R324PaperEndpointParameterizedEE. This file supplies their structural inputs. Each branch retains the genuine alternating transport or retained outgoing stop on which its signed identity is stated, and separately flattens only the common terminal budget into R324PaperHalfCompletedRoute.

No endpoint integral is estimated here. In particular the four literal case costs remain DD, DE, ED, and EE; uniformization is deferred until the two completed halves have been spliced.

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

The paper estimates needed by every structural endpoint route. The exceptional-head provider is indexed by the actual incoming Fourier mode; all other data are mode-independent.

• supportConstant : ℝ

  The common support constant from Proposition 4.1. Endpoint routes retain it because an outgoing exceptional block is estimated only after its signed Fourier defect has been formed.

• supportConstant_pos : 0 < self.supportConstant
• hm : 0 < m
• heps : 0 < eps
• heps1 : eps ≤ 1
• hC : 0 ≤ C
• hlam : 0 ≤ lam
• hK : 1 ≤ K
• hA : 1 ≤ A
• prop41Provider : R324WithinHalfProp41Provider rho C lam eps self.supportConstant pairing
• analyticProvider : R324WithinHalfLocalBlockProvider rho C lam eps K pairing
• budgetProvider : R324WithinHalfBudgetLocalBlockProvider rho C lam eps K A pairing
• headBudget : R324WithinHalfInsertedExceptionalHeadBudget rho C lam eps K pairing incomingMode
• outgoingInsertedBudget (n : ℕ) : 1 ≤ n → 2 * ∫ (z : T4), primitiveInsertedMajorant C lam eps self.supportConstant n z ∂paperMeasure ≤ (C * lam) ^ (2 * n) * K

  The same uniform inserted-kernel budget pays a retained exceptional outgoing block after its signed Fourier defect has been formed. The factor two is the literal Green-difference constant in paper Step 4(A).

• initialCertificate : R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState m) fun (x : Fin (m + 1)) => A

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders.hK_nonneg {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) : 0 ≤ K

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders.initialBudgetReachable {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (_providers : R324PaperHalfRouteProviders pairing incomingMode) : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A (initial rho lam eps pairing).state fun (x : Fin (m + 1)) => A

A reusable nonzero-predecessor fact

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_ne_zero_of_finalActive_lt {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (_hremaining : res.remaining = head :: tail) (i : Fin m) (hiFinal : i ∈ finalActive pairing) (hiLt : i < head.1.1) : r324WithinHalfPredecessorSlot res.state head ≠ 0

A surviving final vertex to the left of a scheduled head is an explicit nonzero predecessor candidate. This is the small geometric fact needed to consume a retained outgoing terminal without changing slot zero.

Branch witness packages

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

• transport : (initial rho lam eps pairing).R324WithinHalfAlternatingTransport
• route : R324PaperHalfCompletedRoute pairing incomingMode
• route_cases : self.route.cases = ![SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.directFourier]
• route_final : self.route.final = self.transport.final
• route_transportedMultiplier : self.route.transportedMultiplier = self.transport.multiplier incomingMode
• route_firstCharge : self.route.firstCharge = A

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

• terminalData : R324ShortcutTerminalSchedule pairing
• trace : R324WithinHalfStopBeforeStepTrace self.terminalData.terminal [] (initial rho lam eps pairing) fun (x : Fin (m + 1)) => A
• ordinary : self.trace.OrdinaryAlong
• stopBudgetScale : Fin (m + 1) → ℝ

  The paper's Step 4(A) outgoing-endpoint estimate is made on the state immediately before the retained terminal is consumed. Keep the synchronized budget on that literal state; the completed route below is the post-terminal carrier and cannot reconstruct this information.

• stopReachable : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A self.trace.stopPrefix.state self.stopBudgetScale
• stopCertificate : R324WithinHalfEdgeCertificate self.trace.stopPrefix.state self.stopBudgetScale
• stopScale_le_budget (edge : Fin (m + 1)) : self.trace.stopScale edge ≤ self.stopBudgetScale edge
• stopBudgetScale_zero_eq_base : self.stopBudgetScale 0 = A

  The direct incoming leg is ordinary throughout the stopped prefix, so the synchronized complete budget keeps its initial boundary value. This is the exact equality returned by the producer; retaining it avoids reconstructing the stopped traversal in Step 4(A).

• endpoint : R324WithinHalfEndpointStopAtTerminal self.terminalData.terminal (initial rho lam eps pairing)
• endpoint_eq : self.endpoint = R324WithinHalfEndpointStopAtTerminal.of_ordinaryTrace self.trace ⋯
• outgoing : (initial rho lam eps pairing).R324PaperOutgoingEndpointTerminal
• outgoing_eq : self.outgoing = { terminalData := self.terminalData, endpoint := self.endpoint }
• predecessor_ne_zero : r324WithinHalfPredecessorSlot self.endpoint.stop.state self.terminalData.terminal ≠ 0

  The retained terminal is genuinely fed from an internal predecessor. This is proved when the literal DE route is selected and is required by the signed outgoing-endpoint identity; it must not be forgotten when the completed post-terminal carrier is formed.

• terminalPost_active : self.outgoing.terminalPost.state.active.Nonempty

  The direct incoming single survives the retained outgoing block, so the post-terminal carrier on which the endpoint defect is evaluated is nonempty.

• route : R324PaperHalfCompletedRoute pairing incomingMode
• route_cases : self.route.cases = ![SmoothCutoff.R324EndpointReductionCase.directFourier, SmoothCutoff.R324EndpointReductionCase.insertedSacrifice]
• route_final : self.route.final = self.outgoing.terminalPost

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

• pack : R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly pairing
• transport : (self.pack.data.trace.stopPrefix.afterHead self.pack.data.terminal self.pack.data.suffix ⋯).R324WithinHalfAlternatingTransport
• route : R324PaperHalfCompletedRoute pairing incomingMode
• route_cases : self.route.cases = ![SmoothCutoff.R324EndpointReductionCase.insertedSacrifice, SmoothCutoff.R324EndpointReductionCase.directFourier]
• route_final : self.route.final = self.transport.final
• multiplier_mul_afterHeadBudgetScale_le_terminalScale_zero : ‖self.transport.multiplier incomingMode‖ * self.pack.afterHeadBudgetScale 0 ≤ self.route.terminalScale 0

  The constructor already proves this stronger, literal after-head budget estimate. Retaining it pays the complete exceptional incoming head before the final direct Fourier operation.

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

• pack : R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly pairing
• terminalData : R324ShortcutTerminalSchedule pairing
• endpoint : R324BudgetedEndpointStopAtTerminal self.terminalData.terminal (self.pack.data.trace.stopPrefix.afterHead self.pack.data.terminal self.pack.data.suffix ⋯) self.pack.afterHeadBudgetScale incomingMode
• outgoing : (self.pack.data.trace.stopPrefix.afterHead self.pack.data.terminal self.pack.data.suffix ⋯).R324PaperOutgoingEndpointTerminal
• outgoing_eq : self.outgoing = { terminalData := self.terminalData, endpoint := self.endpoint.endpoint }
• route : R324PaperHalfCompletedRoute pairing incomingMode
• route_cases : self.route.cases = ![SmoothCutoff.R324EndpointReductionCase.insertedSacrifice, SmoothCutoff.R324EndpointReductionCase.insertedSacrifice]
• route_final : self.route.final = self.outgoing.terminalPost

Direct/direct

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders.exists_directDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) (_hfirst : ⟨0, ⋯⟩ ∈ finalActive pairing) (_hshortcut : Fin.last m ∉ extractedRightEdges pairing) : Nonempty (R324PaperHalfDirectDirectRoute providers)

Genuine all-schedule transport for the DD branch.

Direct/exceptional

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders.exists_directExceptional {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) (hfirst : ⟨0, ⋯⟩ ∈ finalActive pairing) (hshortcut : Fin.last m ∈ extractedRightEdges pairing) : Nonempty (R324PaperHalfDirectExceptionalRoute providers)

Literal DE route: the proper prefix is wholly ordinary, then the canonical outgoing shortcut is retained and consumed exactly once.

Exceptional/direct

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders.exists_exceptionalDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) (hfirst : ⟨0, ⋯⟩ ∉ finalActive pairing) (_hshortcut : Fin.last m ∉ extractedRightEdges pairing) : Nonempty (R324PaperHalfExceptionalDirectRoute providers)

The incoming exceptional head is removed first and its exact signed multiplier is transported through the remaining schedule.

Exceptional/exceptional

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfRouteProviders.exists_exceptionalExceptional {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) (hfirst : ⟨0, ⋯⟩ ∉ finalActive pairing) (hshortcut : Fin.last m ∈ extractedRightEdges pairing) (hsingles : pairing.singles.Nonempty) : Nonempty (R324PaperHalfExceptionalExceptionalRoute providers)

Literal EE route. The first exceptional incoming block is charged before the after-head suffix is traversed. The canonical outgoing shortcut is kept as the last unconsumed block, so the returned outgoing is exactly the dependent witness required by the parameterized signed EE identity.