Compatible analytic and complete-budget traces for R-324

The signed Phase-A collapse and the numerical edge ledger use the same literal within-half suffix, but intentionally update their scales in different ways. The numerical update also charges the outgoing Green edge.

This file constructs the two traces synchronously. Starting from the same uniform all-Green scale, the complete-budget scale dominates the analytic scale slot by slot at every head. Consequently the terminal active product appearing after the signed collapse is controlled by the already proved exact budget-product invariant.

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

One signed analytic trace together with a complete numerical budget on its actual terminal residual state.

• analytic : res.R324WithinHalfCertifiedAnalyticTrace initialScale
• budgetScale : Fin (m + 1) → ℝ
• budgetReachable : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A self.analytic.terminalPrefix.state self.budgetScale
• budgetCertificate : R324WithinHalfEdgeCertificate self.analytic.terminalPrefix.state self.budgetScale
• terminalScale_le (edge : Fin (m + 1)) : self.analytic.terminalScale edge ≤ self.budgetScale edge

theorem Anderson4D.R324WithinHalfResidualPrefix.R324CompatibleAnalyticBudgetTrace.exists_of_providers {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < ε) (hε1 : ε ≤ 1) (hC : 0 < C) (hlam : 0 < lam) (hK : 0 < K) (hA : 1 ≤ A) (analyticProvider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (budgetProvider : R324WithinHalfBudgetLocalBlockProvider ρ C lam ε K A pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (analyticScale budgetScale : Fin (m + 1) → ℝ) (analyticCertificate : R324WithinHalfEdgeCertificate res.state analyticScale) (budgetReachable : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A res.state budgetScale) (budgetCertificate : R324WithinHalfEdgeCertificate res.state budgetScale) (hle : ∀ (edge : Fin (m + 1)), analyticScale edge ≤ budgetScale edge) : Nonempty (res.R324CompatibleAnalyticBudgetTrace analyticScale)

Synchronous recursion through the literal suffix constructs the signed analytic trace and a dominating complete numerical budget on the same terminal residual prefix.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324CompatibleAnalyticBudgetTrace.analytic_activeEdgeScaleProduct_le {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {initialScale : Fin (m + 1) → ℝ} (data : res.R324CompatibleAnalyticBudgetTrace initialScale) : ∏ edge ∈ data.analytic.terminalPrefix.activeEdgeSlots, data.analytic.terminalScale edge ≤ ∏ edge ∈ data.analytic.terminalPrefix.activeEdgeSlots, data.budgetScale edge

The terminal analytic active-scale product is dominated by the exact complete-budget product.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324CompatibleAnalyticBudgetTrace.analytic_activeEdgeScaleProduct_le_closedForm {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {initialScale : Fin (m + 1) → ℝ} (data : res.R324CompatibleAnalyticBudgetTrace initialScale) : ∏ edge ∈ data.analytic.terminalPrefix.activeEdgeSlots, data.analytic.terminalScale edge ≤ (∏ _edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot (r324InitialWithinHalfEdgeState m).active, A) * (C * lam) ^ (2 * r324WithinHalfProcessedOrder data.analytic.terminalPrefix.state) * K ^ data.analytic.terminalPrefix.state.processed.length

Closed form of the complete numerical budget controlling the terminal analytic active product.

Uniform paper-truncation constructor

theorem Anderson4D.exists_r324InitialCompatibleAnalyticBudgetTrace_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ), 0 < supportConstant ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ ∀ (lam ε : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → Nonempty ((R324WithinHalfResidualPrefix.initial ρ lam ε pairing).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A)

Proposition 4.1 constructs a signed analytic trace and a compatible complete numerical budget from the same all-Green root, uniformly in the pairing and order allowed by the paper truncation.