Direct outgoing boundary geometry for R-324

In the direct endpoint branch, the final internal vertex is not removed by the within-half extraction schedule. Thus it is the greatest terminal active vertex, so its outgoing slot is the external slot Fin.last m. Reachability also shows that this external slot is never updated by an analytic collapse. Consequently the completed outgoing boundary edge is exactly greenFn.

theorem Anderson4D.R324WithinHalfStateReachable.edge_finLast_eq_greenFn {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} (hstate : R324WithinHalfStateReachable pairing ρ lam ε state) : state.edges (Fin.last m) = greenFn

The external outgoing slot lies strictly to the right of every analytic step and therefore remains the free Green edge in every reachable state.

theorem Anderson4D.lastInternal_mem_finalActive_of_finLast_not_mem_extractedRightEdges {m : ℕ} (κ : PartialPairing (Fin m)) (hm : 0 < m) (hdirect : Fin.last m ∉ extractedRightEdges κ) : ⟨m - 1, ⋯⟩ ∈ finalActive κ

If the external outgoing edge is not an extracted right edge, the last internal vertex survives the complete reduction schedule.

theorem Anderson4D.R324WithinHalfResidualPrefix.active_nonempty_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hdirect : Fin.last m ∉ extractedRightEdges pairing) : res.state.active.Nonempty

In the direct outgoing branch, a completed within-half state has a nonempty active carrier: the last internal vertex survives.

theorem Anderson4D.R324WithinHalfResidualPrefix.terminalOutgoingEdgeSlot_eq_finLast_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hdirect : Fin.last m ∉ extractedRightEdges pairing) (hactive : res.state.active.Nonempty) : res.terminalOutgoingEdgeSlot hactive = Fin.last m

In the direct outgoing branch, the terminal boundary slot is the external final edge slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.state_edges_terminalOutgoingEdgeSlot_eq_greenFn_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hdirect : Fin.last m ∉ extractedRightEdges pairing) (hactive : res.state.active.Nonempty) : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn

The completed direct outgoing boundary edge is exactly the free Green function. This is the structural input needed by the direct endpoint Fourier transform.

theorem Anderson4D.R324WithinHalfResidualPrefix.state_edges_terminalOutgoingEdgeSlot_eq_greenFn_of_not_shortcut {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hdirect : r324OutgoingIsShortcut pairing = false) (hactive : res.state.active.Nonempty) : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn

Boolean-flag form of the direct outgoing boundary theorem.