Certified traces stopping before an exceptional incoming collapse

If the first internal vertex is removed by the within-half analytic schedule, it belongs to an actual extraction block whose left endpoint is zero. This module constructs the certified residual trace directly from the initial prefix to the state immediately before that block. In particular, the state underlying the incoming exceptional stop is definitionally the state produced by the quantitative trace; no reachability-uniqueness comparison is required.

The retained block and its complete suffix remain unintegrated. This file contains only schedule, certificate, order, and boundary geometry ledgers; no endpoint Fubini exchange is performed.

structure Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} (κ : PartialPairing (Fin m)) (initialScale : Fin (m + 1) → ℝ) : Type

A certified trace from the all-Green initial prefix to immediately before a schedule block beginning at the first internal vertex.

• pre : List (R322ExtractionStep m)
• suffix : List (R322ExtractionStep m)
• terminal : R322ExtractionStep m
• schedule_eq : r322AnalyticSchedule κ = self.pre ++ self.terminal :: self.suffix
• left_eq_zero : ↑self.terminal.1.1 = 0
• trace : R324WithinHalfStopBeforeStepTrace self.terminal self.suffix (initial ρ lam ε κ) initialScale

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stopContext {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : R324WithinHalfStepContext κ

The genuine residual context at the retained exceptional head.

Equations

• data.stopContext = data.trace.stopPrefix.headContext data.terminal data.suffix ⋯

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingStop {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : R324IncomingExceptionalStop ρ lam ε κ

The trace stop, viewed through the local incoming-exceptional API. The residual state is literally the trace's stopping state.

Equations

• data.incomingStop = { ctx := data.stopContext, reachable := ⋯, left_eq_zero := ⋯ }

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_processed_eq_pre {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : data.trace.stopPrefix.state.processed = data.pre

The trace consumes exactly the recorded proper prefix.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_remaining_eq {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : data.trace.stopPrefix.remaining = data.terminal :: data.suffix

The retained literal suffix begins with the exceptional block.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_processed_append_eq_schedule {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : data.trace.stopPrefix.state.processed ++ data.terminal :: data.suffix = r322AnalyticSchedule κ

Processed prefix followed by the exceptional block and its suffix is the complete analytic schedule.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stopScale {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : Fin (m + 1) → ℝ

The scale transported through exactly the recorded prefix.

Equations

• data.stopScale = data.trace.stopScale

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stopCertificate {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : R324WithinHalfEdgeCertificate data.trace.stopPrefix.state data.stopScale

The edge certificate genuinely transported to the exceptional stop.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_remainingOrder_eq {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : data.trace.stopPrefix.remainingOrder = residualBlockOrder data.terminal.2 + (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) data.suffix).sum

Exact order retained at the stop: the exceptional block plus every later block, with neither part absorbed.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.order_ledger {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) data.trace.stopPrefix.state.processed).sum + data.trace.stopPrefix.remainingOrder = (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) (r322AnalyticSchedule κ)).sum

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_predecessorSlot_eq_zero {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : r324WithinHalfPredecessorSlot data.trace.stopPrefix.state data.terminal = 0

The retained exceptional head has incoming predecessor slot zero.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_incomingEdge_eq_greenFn {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) : data.trace.stopPrefix.state.edges 0 = greenFn

At positive order, the incoming external edge is still the untouched free Green kernel immediately before the exceptional collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.stop_predecessorEdge_eq_greenFn {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) : data.trace.stopPrefix.state.edges (r324WithinHalfPredecessorSlot data.trace.stopPrefix.state data.terminal) = greenFn

The named predecessor edge at the exceptional stop is the free Green kernel used by the incoming pre-collapse Fourier identity.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.exists_of_initial_certificate {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (hm : 0 < m) (hremoved : ⟨0, hm⟩ ∉ finalActive κ) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) (initialCertificate : R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState m) initialScale) : Nonempty (R324IncomingExceptionalStopTraceAssembly κ initialScale)

Construct the exceptional-stop package from any certificate for the standard all-Green initial state. The trace is built directly from the same schedule decomposition that selects the exceptional block.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.exists_of_localBlockProvider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (hm : 0 < m) (hremoved : ⟨0, hm⟩ ∉ finalActive κ) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) : ∃ (A : ℝ), 0 < A ∧ Nonempty (R324IncomingExceptionalStopTraceAssembly κ fun (x : Fin (m + 1)) => A)

Standard initialization with one positive uniform all-Green scale.