Quantitative full-pairing traces stopping before the terminal block

The light stop trace retains the exact analytic prefix iteration, but its scale update intentionally omits the outgoing Green scale. This module builds the quantitative companion directly from the complete-budget local provider. It consumes the same literal proper prefix of the canonical full-pairing schedule and leaves the last block untouched, while retaining the budget-reachability witness needed by the exact active-scale product ledger.

Literal budget iteration stopping before one specified block

Full-pairing quantitative stop package

structure Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} (κ : PartialPairing (Fin (2 * q))) : Type

A full-pairing schedule stopped immediately before its canonical last block, with the complete numerical edge budget still attached.

The processed and remaining lists are recorded exactly, not merely up to a permutation, so the product and perturbative-order ledgers can be consumed without reconstructing the budget history.

• base_one_le : 1 ≤ A
• terminalData : R324FullPairingTerminalSchedule κ
• stopPrefix : R324WithinHalfResidualPrefix ρ lam ε κ
• stopScale : Fin (2 * q + 1) → ℝ
• reachable : R324WithinHalfBudgetScaleReachable κ ρ C lam ε K A self.stopPrefix.state self.stopScale
• certificate : R324WithinHalfEdgeCertificate self.stopPrefix.state self.stopScale
• stop_processed_eq_proper : self.stopPrefix.state.processed = self.terminalData.proper
• stop_remaining_eq_singleton : self.stopPrefix.remaining = [self.terminalData.terminal]
• terminal_block_eq_stop_active : self.terminalData.terminal.2 = self.stopPrefix.state.active
• order_ledger : (List.map (fun (step : R322ExtractionStep (2 * q)) => residualBlockOrder step.2) self.stopPrefix.state.processed).sum + self.stopPrefix.remainingOrder = q

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

The retained block still has the global right endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace.stop_remainingOrder_eq_terminal {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (data : R324FullPairingBudgetStopTrace κ) : data.stopPrefix.remainingOrder = residualBlockOrder data.terminalData.terminal.2

The unprocessed perturbative order is exactly the retained block order.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace.stop_processed_append_terminal_eq_schedule {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (data : R324FullPairingBudgetStopTrace κ) : data.stopPrefix.state.processed ++ [data.terminalData.terminal] = r322AnalyticSchedule κ

The stopped processed prefix followed by the terminal block is the complete analytic schedule.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace.activeEdgeScaleProduct_eq {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (data : R324FullPairingBudgetStopTrace κ) : ∏ edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot data.stopPrefix.state.active, data.stopScale edge = (∏ _edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot (r324InitialWithinHalfEdgeState (2 * q)).active, A) * (C * lam) ^ (2 * (List.map (fun (step : R322ExtractionStep (2 * q)) => residualBlockOrder step.2) data.terminalData.proper).sum) * K ^ data.terminalData.proper.length

Exact active-scale product after every proper block has been consumed. This is the quantitative invariant at the point where the terminal Fourier estimate starts.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace.exists_of_initial_certificate {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : κ.IsFull) (hA : 1 ≤ A) (provider : R324WithinHalfBudgetLocalBlockProvider ρ C lam ε K A κ) (initialCertificate : R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState (2 * q)) fun (x : Fin (2 * q + 1)) => A) : Nonempty (R324FullPairingBudgetStopTrace κ)

Construct the quantitative stop package from a fixed uniform initial certificate and the complete-budget local provider.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace.exists_with_uniform_initial_scale {ρ : SmoothCutoff} {C lam ε K : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : κ.IsFull) (provider : ∀ (A : ℝ), 1 ≤ A → R324WithinHalfBudgetLocalBlockProvider ρ C lam ε K A κ) : ∃ (A : ℝ), 1 ≤ A ∧ Nonempty (R324FullPairingBudgetStopTrace κ)

Consumer-facing initialization: choose the repository-wide uniform all-Green scale, then use the provider available at that scale.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetStopTrace.exists_of_prop41 {ρ : SmoothCutoff} {C lam ε : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {supportConstant : ℝ} (hsupport : 0 < supportConstant) (hq : 1 ≤ q) (hκ : κ.IsFull) (hC : 0 < C) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hprop : R324WithinHalfProp41Provider ρ C lam ε supportConstant κ) : ∃ (K : ℝ), 0 < K ∧ ∃ (A : ℝ), 1 ≤ A ∧ Nonempty (R324FullPairingBudgetStopTrace κ)

Proposition 4.1 supplies both numerical constants and the complete budget stop package, uniformly before the perturbative order and pairing.