The genuine stop before an exceptional incoming-boundary collapse

If the first internal vertex does not survive the complete within-half schedule, one actual analytic step removes it. This file constructs the reachable heterogeneous state immediately before that step and proves the two structural facts needed by the paper's endpoint-first Fourier argument:

• the step begins at internal vertex zero, so its predecessor slot is the incoming external slot; and
• before the step, that slot still carries the free Green kernel.

No block integration or endpoint Fubini exchange is performed here.

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

A genuine reachable state stopped immediately before an analytic block whose left endpoint is the first internal vertex.

• ctx : R324WithinHalfStepContext κ
• reachable : R324WithinHalfStateReachable κ ρ lam ε self.ctx.state
• left_eq_zero : ↑self.ctx.step.1.1 = 0

theorem Anderson4D.R324IncomingExceptionalStop.first_mem_step_block {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) (hm : 0 < m) : ⟨0, hm⟩ ∈ stop.ctx.step.2

The first internal vertex belongs to the block waiting at the stop.

theorem Anderson4D.R324IncomingExceptionalStop.predecessorSlot_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) : r324WithinHalfPredecessorSlot stop.ctx.state stop.ctx.step = 0

A step beginning at the first internal vertex has the incoming external slot as its sparse predecessor.

theorem Anderson4D.R324IncomingExceptionalStop.first_mem_state_active {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) (hm : 0 < m) : ⟨0, hm⟩ ∈ stop.ctx.state.active

The first internal vertex is active immediately before the exceptional step.

theorem Anderson4D.R324IncomingExceptionalStop.state_edge_zero_eq_greenFn {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) (hm : 0 < m) : stop.ctx.state.edges 0 = greenFn

Before the exceptional step is absorbed, its incoming predecessor is still the untouched free Green edge.

theorem Anderson4D.R324IncomingExceptionalStop.state_edge_predecessor_eq_greenFn {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (stop : R324IncomingExceptionalStop ρ lam ε κ) (hm : 0 < m) : stop.ctx.state.edges (r324WithinHalfPredecessorSlot stop.ctx.state stop.ctx.step) = greenFn

The named predecessor edge used by the stopped step is literally the free Green function.

theorem Anderson4D.exists_r324IncomingExceptionalStop (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (hm : 0 < m) (hremoved : ⟨0, hm⟩ ∉ finalActive κ) : Nonempty (R324IncomingExceptionalStop ρ lam ε κ)

If the first internal vertex is removed by the full analytic schedule, there is a genuine reachable pre-step state of the preceding form.