Certified stop traces for the outgoing-shortcut branch

If the final chain edge is extracted, the analytic schedule has a canonical last step even when the pairing has residual singles. This module combines that terminal schedule with the generic certified prefix iterator. It consumes exactly the proper prefix and leaves the terminal block visible.

Unlike the full-pairing assembly, the terminal block is only the part of the stop active carrier lying in its endpoint interval. No exhaustion of the active carrier, trivial outer factor, or fullness property is asserted.

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

A shortcut terminal schedule together with a certified trace through exactly its proper prefix.

• terminalData : R324ShortcutTerminalSchedule κ
• trace : R324WithinHalfStopBeforeLastTrace self.terminalData.terminal (initial ρ lam ε κ) initialScale

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

The trace consumes exactly the proper part of the canonical terminal schedule.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.stop_remaining_eq_singleton {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324ShortcutStopTraceAssembly κ initialScale) : data.trace.stopPrefix.remaining = [data.terminalData.terminal]

The trace retains exactly the canonical outgoing-shortcut step.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.terminal_block_eq_stop_active_inter_Icc {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324ShortcutStopTraceAssembly κ initialScale) : data.terminalData.terminal.2 = data.trace.stopPrefix.state.active ∩ Finset.Icc data.terminalData.terminal.1.1 data.terminalData.terminal.1.2

For a residual pairing, the retained terminal block is the intersection of the stop active carrier with its ambient endpoint interval.

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

The retained step ends at the final internal vertex.

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

The scale transported through all proper blocks.

Equations

• data.stopScale = data.trace.stopScale

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

The edge certificate transported to the stop state.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.order_ledger {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324ShortcutStopTraceAssembly κ 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.R324ShortcutStopTraceAssembly.exists_of_initial_certificate {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (hshortcut : Fin.last m ∈ extractedRightEdges κ) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) (initialCertificate : R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState m) initialScale) : Nonempty (R324ShortcutStopTraceAssembly κ initialScale)

Construct the shortcut package from any certificate for the all-Green initial state. No fullness hypothesis is used.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324ShortcutStopTraceAssembly.exists_of_localBlockProvider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (hshortcut : Fin.last m ∈ extractedRightEdges κ) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) : ∃ (A : ℝ), 0 < A ∧ Nonempty (R324ShortcutStopTraceAssembly κ fun (x : Fin (m + 1)) => A)

Standard initialization with one positive uniform scale.