Direct incoming boundary geometry for R-324

The incoming external edge is slot zero. A collapse can overwrite that slot only when its block has no surviving internal predecessor. Therefore, as long as the first internal vertex survives, slot zero is untouched and still carries the free Green kernel.

This is deliberately only the direct incoming branch. If the first internal vertex is removed, the paper integrates the incoming Fourier variable before the responsible collapse; the completed slot-zero kernel is then generally not greenFn.

theorem Anderson4D.R324WithinHalfStateReachable.edge_zero_eq_greenFn_of_first_mem_active {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} (hstate : R324WithinHalfStateReachable pairing ρ lam ε state) (hm : 0 < m) (hfirst : ⟨0, hm⟩ ∈ state.active) : state.edges 0 = greenFn

If the first internal vertex is active in a reachable state, the incoming external edge has never been updated.

theorem Anderson4D.R324WithinHalfResidualPrefix.state_edges_zero_eq_greenFn_of_first_mem_finalActive {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hfirst : ⟨0, hm⟩ ∈ finalActive pairing) : res.state.edges 0 = greenFn

Completed-schedule form of the direct incoming boundary theorem.

theorem Anderson4D.R324WithinHalfResidualPrefix.state_edges_zero_eq_greenFn_of_first_not_mem_extractionBlocks {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hfirst : ⟨0, hm⟩ ∉ finsetUnionList (extractionBlocks pairing)) : res.state.edges 0 = greenFn

The same conclusion with the direct incoming branch expressed as non-membership in the union of extracted primitive blocks.