The single-scale permutation estimate

This module closes Proposition 5.10. The proof keeps the completed base-scale coefficient common across the full finite Fubini sum, consumes the outer payoff exactly once, and only then converts the distinguished leaf power to the branch-scale ledger.

noncomputable def Anderson4D.XYCluster.singleScaleFinalExponentialBase (Cfiber Couter : ℝ) : ℝ

The single exponential base left after the inner, outer, occurrence, position, and reverse-power ledgers have all been combined.

Equations

• Anderson4D.XYCluster.singleScaleFinalExponentialBase Cfiber Couter = Anderson4D.XYCluster.finAnchorNXFiberSharpBase Cfiber * Couter * (8 * Real.exp 4) ^ 5

theorem Anderson4D.XYCluster.singleScaleFinalExponentialBase_nonneg (Cfiber Couter : ℝ) (hCfiber : 0 ≤ Cfiber) (hCouter : 0 ≤ Couter) : 0 ≤ singleScaleFinalExponentialBase Cfiber Couter

theorem Anderson4D.XYCluster.singleScale_estimate : ∃ (C0 : ℝ), SingleScaleEstimate C0

The main single-scale permutation-sum theorem.

theorem Anderson4D.singleScale_estimate : ∃ (C0 : ℝ), SingleScaleEstimate C0

Public namespace alias for Proposition 5.10.