Future-edge invariance of the R-322 budget scales

The analytic schedule has strictly increasing right endpoints. Its quantitative scale update changes only the predecessor slot, strictly to the left of the current block. Hence every slot to the right of all processed blocks still carries the initial Green scale. In particular, the outgoing slot of the next block has exactly that scale.

This closes the numerical premise exposed by the complete active-edge ledger: choosing the initial Green scale at least one gives 1 ≤ scale outgoingEdge at every production step without discarding any coupling power.

inductive Anderson4D.R322AnalyticBudgetScaleReachable {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (C lam ε K A : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : R322AnalyticEdgeState q hq → (Fin (2 * q - 1) → ℝ) → Prop

Reachability of a quantitative budget scale along the same genuine proper-step history as the analytic edge state.

• initial {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ (r322InitialAnalyticEdgeState q hq) fun (x : Fin (2 * q - 1)) => A
• update {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (ctx : R322AnalyticProperStepContext q hq) (hpairing : ctx.pairing = κ) (previous : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ ctx.state scale) : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ (ctx.nextState ρ lam ε) (ctx.budgetUpdatedEdgeScale scale C lam K)

theorem Anderson4D.R322AnalyticProperStepContext.budgetUpdatedEdgeScale_eq_of_right_lt {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (C lam K : ℝ) (edge : Fin (2 * q - 1)) (hright : ctx.step.1.2 < r322AnalyticEdgeLeftVertex edge) : ctx.budgetUpdatedEdgeScale scale C lam K edge = scale edge

A budget update leaves every edge strictly to the right of the current block unchanged.

theorem Anderson4D.R322AnalyticBudgetScaleReachable.edgeScale_eq_base_of_processed_right_lt {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {state : R322AnalyticEdgeState q hq} {scale : Fin (2 * q - 1) → ℝ} (hreach : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ state scale) (edge : Fin (2 * q - 1)) (hfuture : ∀ earlier ∈ state.processed, earlier.1.2 < r322AnalyticEdgeLeftVertex edge) : scale edge = A

Every scale slot strictly beyond all processed right endpoints still equals the initial Green scale.

theorem Anderson4D.R322AnalyticBudgetScaleReachable.outgoingEdgeScale_eq_base {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {state : R322AnalyticEdgeState q hq} {scale : Fin (2 * q - 1) → ℝ} (hreach : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ state scale) (ctx : R322AnalyticProperStepContext q hq) (hpairing : ctx.pairing = κ) (hstateEq : ctx.state = state) : scale ctx.outgoingEdge = A

The outgoing scale of the next genuine proper step is exactly the initial Green scale.

theorem Anderson4D.R322AnalyticBudgetScaleReachable.edgeCertificate_to_budgetUpdatedEdgeScale {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {state : R322AnalyticEdgeState q hq} {scale : Fin (2 * q - 1) → ℝ} (hreach : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ state scale) (ctx : R322AnalyticProperStepContext q hq) (hpairing : ctx.pairing = κ) (hstateEq : ctx.state = state) (hA : 1 ≤ A) (hcert : R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (r322AnalyticUpdatedEdgeScale ctx scale (r322AnalyticInternalEdgeScaleProduct ctx scale) C lam K)) : R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (ctx.budgetUpdatedEdgeScale scale C lam K)

A base scale at least one discharges the outgoing normalization premise of the complete budget-certificate update.

Initial normalization

theorem Anderson4D.exists_r322InitialAnalyticEdgeCertificate_one_le (q : ℕ) (hq : 1 ≤ q) : ∃ (A : ℝ), 1 ≤ A ∧ R322AnalyticEdgeCertificate (r322InitialAnalyticEdgeState q hq) fun (x : Fin (2 * q - 1)) => A

The all-Green initial certificate may be chosen with a scale at least one.

theorem Anderson4D.exists_r322InitialAnalyticEdgeCertificate_one_le_uniform : ∃ (A : ℝ), 1 ≤ A ∧ ∀ (q : ℕ) (hq : 1 ≤ q), R322AnalyticEdgeCertificate (r322InitialAnalyticEdgeState q hq) fun (x : Fin (2 * q - 1)) => A

One initial Green scale works simultaneously at every perturbative order. This quantifier order is needed when the final P-3.5a constant is chosen before q.