Geometry at the endpoint-stop terminal

This module identifies the stopped prefix produced by R324WithinHalfEndpointStopAtTerminal with the canonical proper prefix of an outgoing-shortcut terminal schedule. It is the trace-free analogue of R324ShortcutStopTraceAssembly: the terminal block remains visible, its carrier and right endpoint are identified, and its outgoing edge is still the free Green kernel.

Only schedule and edge-state geometry is recorded here. No Fourier integration, ordinary-J estimate, or numerical bound is used.

structure Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} (κ : PartialPairing (Fin m)) : Type

A canonical outgoing-shortcut terminal schedule together with the signed/phased endpoint-stop transport from the initial within-half state.

• terminalData : R324ShortcutTerminalSchedule κ
• transport : R324WithinHalfEndpointStopAtTerminal self.terminalData.terminal (initial ρ lam ε κ)

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.exists_of_localBlockProvider {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {C K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate (initial ρ lam ε κ).state scale) (terminalData : R324ShortcutTerminalSchedule κ) : Nonempty (R324WithinHalfEndpointTerminalGeometry κ)

Construct the canonical terminal geometry directly from the same local block provider and initial edge certificate used by the complete within-half driver. The only change is that the final shortcut block is retained for the endpoint Fourier operation required in paper Step 4.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.stop_processed_eq_proper {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : data.transport.stop.state.processed = data.terminalData.proper

The endpoint-stop driver has consumed exactly the canonical proper prefix before the shortcut terminal.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.stop_remaining_eq_singleton {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : data.transport.stop.remaining = [data.terminalData.terminal]

The stopped residual retains exactly the canonical shortcut terminal.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.terminal_block_eq_stop_active_inter_Icc {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : data.terminalData.terminal.2 = data.transport.stop.state.active ∩ Finset.Icc data.terminalData.terminal.1.1 data.terminalData.terminal.1.2

At the stop, the terminal block is its ambient endpoint interval intersected with the still-active carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.terminal_right_eq_last {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : ↑data.terminalData.terminal.1.2 = m - 1

The retained terminal ends at the final internal vertex.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.terminalContext {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : R324WithinHalfStepContext κ

The retained terminal as a generic within-half step context.

Equations

• data.terminalContext = data.transport.stop.headContext data.terminalData.terminal [] ⋯

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.terminalContext_outgoing_eq_greenFn {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : data.terminalContext.state.edges data.terminalContext.outgoingSlot = greenFn

Reachability keeps the outgoing named edge of the unabsorbed terminal equal to the free Green kernel.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.order_ledger {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) data.transport.stop.state.processed).sum + data.transport.stop.remainingOrder = (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) (r322AnalyticSchedule κ)).sum

Exact processed/remaining perturbative-order ledger at the endpoint stop.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.stop_remainingOrder_eq_terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry κ) : data.transport.stop.remainingOrder = residualBlockOrder data.terminalData.terminal.2

Because the stopped remaining list is a singleton, its retained order is exactly the order of the named terminal block.