ShellEpsPinFloor

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

1. The floor arithmetic

2. The pin, produced

theorem Algsuperdiff.Section4.Provider.Regularity.exists_cedosFloor_shellEpsPin (d : ℕ) : ∃ (Cann : ℝ), 0 < Cann ∧ ∀ (A : ℝ), 0 < A → ∃ (Cfl : ℝ), 1 ≤ Cfl ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → ∀ (Cedos Citer : ℝ) (k : ℕ), Cfl ≤ Cedos → ∀ (alpha : ℝ), 0 < alpha → alpha < 1 → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos 1 Citer k) alpha) → ∀ (j : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ stepThreeGoodEvent M (stepOneDelta (stepOneC1 d Cedos 1 Citer k) alpha) j z → ∀ (L : ℤ), j ≤ L → A * Support.fluxCorrectedErrorRepresentative M L j ⟨stepOneSEighth, stepOneSEighth_pos⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ stepOneS ^ 4

The ε-pin's shell scalar, produced from a C_edos floor.

For every A > 0 there is a floor C_fl ≥ 1 such that, for every C_edos ≥ C_fl, almost surely, on the Step-3/Step-7 good event at this lane's own δ = δ(C₁,α) and at every truncation L ≥ j,

   A · 𝓔_j(z)  ≤  s⁴ ,      s = stepOneS = 1/4 .

This is the hypothesis's exists_boundaryScalar_le_displayLegs_of_epsPin carries, delivered by the lane's own free parameter.