Exact product invariant for the quantitative R-322 schedule

The slotwise budget update has an exact active-edge product recurrence. This module iterates that recurrence over a genuinely reachable scale history and then combines it with the schedule's exact perturbative-order ledger.

def Anderson4D.r322AnalyticProcessedOrder {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) : ℕ

Total perturbative order already absorbed into a sparse edge state.

Equations

• Anderson4D.r322AnalyticProcessedOrder state = (List.map (fun (step : Anderson4D.R322ExtractionStep (2 * q)) => Anderson4D.residualBlockOrder step.2) state.processed).sum

theorem Anderson4D.r322AnalyticActiveEdges_initial (q : ℕ) (hq : 1 ≤ q) : r322AnalyticActiveEdges (r322InitialAnalyticEdgeState q hq) = Finset.univ

theorem Anderson4D.R322AnalyticBudgetScaleReachable.activeEdgeScaleProduct_eq {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 ∈ r322AnalyticActiveEdges state, scale edge = A ^ (2 * q - 1) * (C * lam) ^ (2 * r322AnalyticProcessedOrder state) * K ^ state.processed.length

Exact active-edge product after any quantitatively reachable proper prefix. Every proper block contributes its order power and one collapse constant exactly once.

theorem Anderson4D.R322AnalyticTerminalStepContext.activeEdgeScaleProduct_mul_terminalPower {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (hpairing : ctx.pairing = κ) (hreach : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ ctx.state scale) : (∏ edge ∈ r322AnalyticActiveEdges ctx.state, scale edge) * (C * lam) ^ (2 * residualBlockOrder ctx.terminal.2) = A ^ (2 * q - 1) * (C * lam) ^ (2 * q) * K ^ ctx.state.processed.length

After adding the final primitive block, the coupling power is exactly the ambient perturbative order 2q; no block order is lost or duplicated.

theorem Anderson4D.R322AnalyticTerminalStepContext.budgetMultiplier_le_finalEvenPower {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) {K A : ℝ} (hA : 1 ≤ A) (hK : 0 < K) : A ^ (2 * q - 1) * K ^ ctx.state.processed.length ≤ (A * max 1 K) ^ (2 * q)

The initial Green scales and the one constant per proper collapse can be absorbed into a single base raised to the final even order.

theorem Anderson4D.R322AnalyticTerminalStepContext.activeEdgeScaleProduct_mul_terminalMajorant_le {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (hpairing : ctx.pairing = κ) (hreach : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ ctx.state scale) (hA : 1 ≤ A) (hK : 0 < K) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (supportConstant : ℝ) (z : T4) : (∏ edge ∈ r322AnalyticActiveEdges ctx.state, scale edge) * primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.terminal.2) z ≤ primitiveKernelMajorant (A * max 1 K * C) lam ε supportConstant q z

Exact terminal-order accounting plus the preceding numerical absorption turn the residual-block majorant into one ambient-order majorant.

theorem Anderson4D.R322AnalyticTerminalStepContext.abs_terminalSpatialIntegral_le_finalMajorant {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) {ρ : SmoothCutoff} {C lam ε K A : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (hpairing : ctx.pairing = κ) (hreach : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ ctx.state scale) (hA : 1 ≤ A) (hK : 0 < K) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (supportConstant : ℝ) (hcert : R322AnalyticEdgeCertificate ctx.state scale) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.terminal.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ H supportConstant C) (z : T4) (hz : z ≠ 0) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.terminal.2))), MeasureTheory.Integrable (fun (u : Fin (2 * residualBlockOrder ctx.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.terminal.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.terminal.2) ⋯ z 0 u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.terminal.2 - 2)) => paperMeasure)) : |ctx.terminalSpatialIntegral ρ lam ε z 0| ≤ primitiveKernelMajorant (A * max 1 K * C) lam ε supportConstant q z

Fully quantitative terminal Proposition 4.1 estimate in the final ambient-order normalization. The remaining R-322 work is to identify each fixed endpoint fibre with this terminal spatial integral.