Certified full-pairing traces stopping at the terminal block

For a full pairing on an even carrier, the analytic schedule has a canonical last block. This module combines that terminal schedule with the generic within-half prefix iterator: all proper blocks are consumed, while the last block and its global right endpoint remain visible for the final Fourier estimate.

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

A full-pairing terminal schedule together with a certified analytic trace through precisely its proper prefix.

• terminalData : R324FullPairingTerminalSchedule κ
• trace : R324WithinHalfStopBeforeLastTrace self.terminalData.terminal (initial ρ lam ε κ) initialScale
• terminal_block_eq_stop_active : self.terminalData.terminal.2 = self.trace.stopPrefix.state.active
• order_ledger : (List.map (fun (step : R322ExtractionStep (2 * q)) => residualBlockOrder step.2) self.trace.stopPrefix.state.processed).sum + self.trace.stopPrefix.remainingOrder = q

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

The retained terminal block ends at the global right endpoint.

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

The scale transported through all proper within-half blocks.

Equations

• data.stopScale = data.trace.stopScale

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.stopProjection {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324FullPairingStopTraceAssembly κ initialScale) : ((initial ρ lam ε κ).SurvivingCoordinate → T4) → data.trace.stopPrefix.SurvivingCoordinate → T4

The coordinate restriction transported through all proper blocks.

Equations

• data.stopProjection = data.trace.stopProjection

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

The terminal edge certificate after all proper blocks have been consumed.

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

The trace retains exactly the canonical terminal step.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.exists_of_initial_certificate {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (hq : 1 ≤ q) (hκ : κ.IsFull) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) (initialCertificate : R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState (2 * q)) initialScale) : Nonempty (R324FullPairingStopTraceAssembly κ initialScale)

Construct the terminal package from any certificate for the standard all-Green initial prefix.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingStopTraceAssembly.exists_of_localBlockProvider {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : κ.IsFull) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κ) : ∃ (A : ℝ), 0 < A ∧ Nonempty (R324FullPairingStopTraceAssembly κ fun (x : Fin (2 * q + 1)) => A)

Consumer-facing standard initialization: choose one positive uniform all-Green scale, then stop the certified trace at the canonical last block.