UpperCollarBandMeanDepthChoice

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

The source-compatible depth coefficient for the collar band-mean lane

The source chooses k₀ = ceil (c E⁻² gamma⁻¹) with a sufficiently small positive dimension-dependent c. The coefficient 1 used by earlier upper profiles is too large for the first collar-density exponential after the square-root/fourth-root interpolation. This file records that scalar mismatch and selects a smaller coefficient from the proved percolation rate.

Nothing here changes a source-facing declaration or makes a source-node or development-status claim.

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

A positive source-compatible coefficient for k₀ = ceil (c E⁻² gamma⁻¹).

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthCoeff d = Algsuperdiff.Section3.Provider.Percolation.siteRateBase d / 64

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepth {d : ℕ} (M : ABKModel d) (E : ℝ) : ℕ

The internally selected integer depth.

Equations

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

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

The room left below the Step-3 mass-density ceiling (siteRateBase d / 2) E⁻² gamma⁻¹.

Equations

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

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

A dimension-only lower bound on E⁻² gamma⁻¹ that pays both the three-layer floor and the one-unit ceiling error.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthCoeff_pos (d : ℕ) : 0 < collarBandMeanDepthCoeff d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthCoeff_le_one (d : ℕ) : collarBandMeanDepthCoeff d ≤ 1

@[simp]

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthSlack_eq (d : ℕ) : collarBandMeanDepthSlack d = 31 * Percolation.siteRateBase d / 64

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthSlack_pos (d : ℕ) : 0 < collarBandMeanDepthSlack d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthThreshold_pos (d : ℕ) : 0 < collarBandMeanDepthThreshold d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.three_le_waveBandDepth_collarBandMeanDepthCoeff {d : ℕ} {E gamma X : ℝ} (hE : 0 < E) (hgamma : 0 < gamma) (hX : X = E⁻¹ ^ 2 * gamma⁻¹) (hlarge : collarBandMeanDepthThreshold d ≤ X) : 3 ≤ waveBandDepth (collarBandMeanDepthCoeff d) E gamma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandDepth_collarBandMeanDepthCoeff_le_siteRate {d : ℕ} {E gamma X : ℝ} (hE : 0 < E) (hgamma : 0 < gamma) (hX : X = E⁻¹ ^ 2 * gamma⁻¹) (hlarge : collarBandMeanDepthThreshold d ≤ X) : ↑(waveBandDepth (collarBandMeanDepthCoeff d) E gamma) ≤ Percolation.siteRateBase d / 2 * X

The selected ceiling satisfies the exact Step3Seams.hk0 density window once the dimension-only threshold pays its one-unit rounding error.