One coherent budget and terminal-Fourier package for a full pairing

The numerical budget trace and the analytic terminal geometry are built with different scale updates: the budget update also charges the outgoing Green edge. Their scale functions therefore must not be identified. Nevertheless, their reached residual state is canonical, because both have consumed the same literal proper prefix of the analytic schedule.

This module records that state identification explicitly. Downstream arguments can use the complete budget product and the exact terminal Fourier identity from one package, without silently assuming that two independently constructed stop states coincide.

theorem Anderson4D.R324WithinHalfStateReachable.eq_of_processed_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {left right : R324WithinHalfEdgeState m} (hleft : R324WithinHalfStateReachable pairing ρ lam ε left) (hright : R324WithinHalfStateReachable pairing ρ lam ε right) (hprocessed : left.processed = right.processed) : left = right

Algebraic reachability is deterministic once the processed schedule prefix is fixed.

theorem Anderson4D.R324FullPairingTerminalSchedule.unique {m : ℕ} {κ : PartialPairing (Fin m)} (left right : R324FullPairingTerminalSchedule κ) : left = right

The decomposition of a nonempty analytic schedule into its proper prefix and singleton final step is unique.

theorem Anderson4D.R324WithinHalfResidualPrefix.eq_of_state_eq_of_remaining_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (left right : R324WithinHalfResidualPrefix ρ lam ε pairing) (hstate : left.state = right.state) (hremaining : left.remaining = right.remaining) : left = right

Residual prefixes are determined by their algebraic state and literal remaining suffix; the schedule and reachability fields are propositions.

theorem Anderson4D.R324WithinHalfResidualPrefix.eq_of_processed_schedule_of_remaining_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (left right : R324WithinHalfResidualPrefix ρ lam ε pairing) (hleftProcessed : left.state.processed = r322AnalyticSchedule pairing) (hrightProcessed : right.state.processed = r322AnalyticSchedule pairing) (hleftRemaining : left.remaining = []) (hrightRemaining : right.remaining = []) : left = right

Two residual prefixes which have consumed the complete analytic schedule are the same dependent carrier. This is the reusable terminal uniqueness form of R324WithinHalfStateReachable.eq_of_processed_eq: the edge state is forced by reachability and the processed list, while both remaining suffixes are empty.

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

One package carrying both the complete numerical budget and the exact terminal analytic/Fourier view.

The scale functions are intentionally kept separate. The equality field identifies only the reached residual prefix, which is precisely the object on which the terminal geometry depends.

• initialScale : Fin (2 * q + 1) → ℝ
• geometry : R324FullPairingStopTraceAssembly κ self.initialScale
• terminalData_eq : self.geometry.terminalData = budget.terminalData
• stopPrefix_eq : self.geometry.trace.stopPrefix = budget.stopPrefix

def Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.ofAssembly {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} {initialScale : Fin (2 * q + 1) → ℝ} (geometry : R324FullPairingStopTraceAssembly κ initialScale) : R324FullPairingBudgetTerminalAdapter budget

Any analytic terminal assembly for the same pairing canonically adapts to a quantitative budget stop: algebraic reachability and the literal processed prefix force the two residual states to agree.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.ofAssembly geometry = { initialScale := initialScale, geometry := geometry, terminalData_eq := ⋯, stopPrefix_eq := ⋯ }

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.reachable {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) : R324WithinHalfBudgetScaleReachable κ ρ C lam ε K A data.geometry.trace.stopPrefix.state budget.stopScale

The complete budget reachability witness remains attached to the same reached state used by geometry.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.certificate {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) : R324WithinHalfEdgeCertificate data.geometry.trace.stopPrefix.state budget.stopScale

The complete edge certificate remains attached to the same reached state used by geometry.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.activeEdgeScaleProduct_eq {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) : ∏ edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot data.geometry.trace.stopPrefix.state.active, budget.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) budget.terminalData.proper).sum) * K ^ budget.terminalData.proper.length

Exact complete active-scale product, written on the analytic geometry state identified by this adapter.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integral_char_mul_terminal_rawLocal_translated {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (β : Z4) (x : T4) (t : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2) → T4) : ∫ (y : T4), charT4 β y * ↑((data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).step.2)) => t j - y) ∂paperMeasure = ↑(data.geometry.terminalGroupedPrimitiveCore x t) * r324EndpointCoefficient β (t (primitiveLast (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯)) (t ⟨0, ⋯⟩) true

Exact terminal endpoint-first Fourier identity on the residual state which also carries the complete budget witness. The primitive-pairing sum remains grouped inside terminalGroupedPrimitiveCore.