PerCubeGaugeBounds

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Step 5's per-cube evaluation: the gauge bounds

What this module supplies

The proved per-cube moments (PerCubeFirstThird, SecondTermMoment) carry SYMBOLIC majorants: products of the Step-4 bullets' own constants, σ-gauges and 3^{γ·} weights. Step 5's evaluation needs them read against the anchor's own scalar, so each symbolic ingredient must be converted into (dimension, c⋆)-constants times powers of γ, s, q and 3^{γ(m−j)}. This module performs exactly those conversions, and nothing else:

1. The geometric constants, uniformized. fullGradConst and deepGradConst both carry the γ-dependent factor (1 − 3^{γ−1})^{-1}; SecondTermArithmetic.inv_one_sub_rpow_three_gamma_le prices it at 3, so both become dimensional.
2. The λ-slot majorant, factored. lambdaSlotMajorant is σ_{j−1}^{-1} · lambdaSlotFactor, and the factor is bounded by an absolute constant on the anchor's own moment range r ≤ γ^{-1}: the printed q³ e^{−C^{-1}γ^{-1}} of bullet (B5)'s moment conversion is O(1) there, by SecondTermArithmetic.pow_mul_exp_neg_inv_le.
3. The four σ gauge facts, packaged at one constant: bullet (B3) at the (B5) index j−1 and at the index m, bullet (B1), and the σ_{j−2}/σ_{j−1} reconciliation.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4 bullets (B1)/(B3)/(B5)/(B6a).

theorem Algsuperdiff.Section4.Provider.BoundsEaL.rpowBridgeGauge (x y : ℝ) : x.rpow y = x ^ y

The prefix spelling Real.rpow x y and the notation x ^ y are the same term. Local re-derivation of Step5GeometricClosure's private rpowBridge.

1. The geometric constants, uniformized

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.fullGradBound (d : ℕ) : ℝ

The dimensional bound on GradBottomLayer.fullGradConst.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.fullGradBound d = HCPolySupport.IndependentSums.gammaTriangleConst 2 * ((Algsuperdiff.Section4.Provider.BoundsEaL.bottomGradConst d + 3) * 3)

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.deepGradBound : ℝ

The absolute bound on GradSlotMoment.deepGradConst.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.deepGradBound = HCPolySupport.IndependentSums.gammaTriangleConst 2 * 3

theorem Algsuperdiff.Section4.Provider.BoundsEaL.fullGradBound_pos (d : ℕ) : 0 < fullGradBound d

theorem Algsuperdiff.Section4.Provider.BoundsEaL.deepGradBound_pos : 0 < deepGradBound

theorem Algsuperdiff.Section4.Provider.BoundsEaL.fullGradConst_le {d : ℕ} (M : Section3.ABKModel d) (hgam : M.gamma ≤ 1 / 2) : fullGradConst M ≤ fullGradBound d

theorem Algsuperdiff.Section4.Provider.BoundsEaL.deepGradConst_le {d : ℕ} (M : Section3.ABKModel d) (hgam : M.gamma ≤ 1 / 2) : deepGradConst M ≤ deepGradBound

2. The λ-slot majorant, factored

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.lambdaSlotFactor (d : ℕ) (M : Section3.ABKModel d) (E r : ℝ) : ℝ

The σ-free factor of lambdaSlotMajorant.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lambdaSlotMajorant_eq_mul (d : ℕ) (M : Section3.ABKModel d) (E : ℝ) (j : ℤ) (r : ℝ) : lambdaSlotMajorant d M E j r = (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ * lambdaSlotFactor d M E r

The λ-slot majorant is σ_{j−1}^{-1} times a σ-free factor.

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.lambdaSlotFactorBound (d : ℕ) (E : ℝ) : ℝ

The absolute bound on the σ-free factor, at the budget E.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lambdaSlotFactorBound_pos (d : ℕ) {E : ℝ} (hE : 0 < E) : 0 < lambdaSlotFactorBound d E

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lambdaSlotFactor_le (d : ℕ) (M : Section3.ABKModel d) {E r : ℝ} (hE : 0 < E) (hr : 0 ≤ r) (hrg : r ≤ M.gamma⁻¹) : lambdaSlotFactor d M E r ≤ lambdaSlotFactorBound d E

Bullet (B5)'s q³ e^{−C^{-1}γ^{-1}} is O(1) on the printed range.

On the anchor's own moment range r ≤ γ^{-1} -- which its p-range p ≤ C^{-1}γ^{-1}s delivers -- the σ-free factor of the (B5) majorant is at most an absolute constant. No p-restriction beyond the printed one is used.

3. The four σ gauge facts, packaged

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_sigmaBar_gaugePackage (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → (∀ (j : ℤ), 3 ^ (M.gamma * ↑j) * (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 16 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)) ∧ (∀ (m : ℤ), 3 ^ (M.gamma * ↑m) * (↑(Section3.Annealed.sigmaBar M m))⁻¹ ≤ 4 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)) ∧ (∀ (m j : ℤ), j - 2 ≤ m → (↑(Section3.Annealed.sigmaBar M m))⁻¹ * ↑(Section3.Annealed.sigmaBar M (j - 2)) ≤ 4) ∧ ∀ (j : ℤ), ↑(Section3.Annealed.sigmaBar M (j - 2)) * (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 4

The gauge package.

At one constant, in the printed regime alone: bullet (B3) at the (B5) index j−1 (constant 16, SigmaBarLandmark), bullet (B3) at the index m (constant 4, StepFourSigmaBar read at m+2), bullet (B1), and the σ_{j−2}/σ_{j−1} reconciliation.