SuperposedFluxLowerAssembly

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

Assembly of the sharp lower coarse-ellipticity lane

One explicit dimension-only constant below dominates the auxiliary profile, all three deterministic branch constants, and all three rare-event budgets. The finite subquadratic, finite superquadratic, and infinity payloads are then combined and converted to the literal lower-family carrier. The final theorem has exactly the lower conjunct's exported binders; all scalar gate choices and the small/large scale split remain inside its proof.

This is a proved lower-leg declaration only. It does not assert status for the frozen two-sided coarse-ellipticity theorem or for any source node.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLowerConst (d : ℕ) : ℝ

A single dimension-only output constant for the sharp lower lane. The max 0 wrappers make positivity unconditional in the ambient natural-number dimension; an actual ABKModel d later supplies its standing 2 ≤ d.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.eight_le_superposedFluxLowerConst (d : ℕ) : 8 ≤ superposedFluxLowerConst d

The assembled lower-profile budget includes the fixed margin eight.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLowerConst_pos (d : ℕ) : 0 < superposedFluxLowerConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_coarse_ellipticity_lower_large_scale {d : ℕ} (M : ABKModel d) (m : ℤ) (_hm : mStar M < m) (E : { E : ℝ // 1 ≤ E }) (hstate : Frozen.Section3.inductionState M (m - 1) E) (sigma : ℝ) (hsigma : sigma ∈ Set.Ioc 0 (1 / 2)) (hE1 : max (Real.exp (superposedFluxLowerConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hE2 : ↑E ≤ M.gamma ^ (-(1 / 5))) (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-((superposedFluxLowerConst d)⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1) : Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile (superposedFluxLowerConst d) M.gamma s q) (Real.exp (-((superposedFluxLowerConst d)⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The exact frozen lower-family carrier in the internal large-scale branch. The branch condition is a splice input and does not occur in the conclusion.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_coarse_ellipticity_lower_leg (d : ℕ) : ∃ (Clow : ℝ), 0 < Clow ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile Clow M.gamma s q) (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

Literal lower-conjunct theorem for the sharp lower lane. The only exported data are those of the frozen lower-family statement; the scale split and every scalar adequacy inequality are discharged internally.