StepSevenFlushHgradSlot

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

4. The abstract assembly core

5. The flush branch's hgrad slot

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenFlushHgrad (d : ℕ) {M : Section3.ABKModel d} {nroot n m : ℤ} {z : HCPolySupport.Vec d} (uglob : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {K1 K2 Khol Kh Cosc oscHi oscData C1 alpha delta : ℝ} {B : ℕ} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnrootm : nroot ≤ m) (hcore : nroot + 1 ≤ n) (hn3m : n + 3 ≤ m) (hC1 : 2 * ↑d + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hgap : n + 2 - nroot ≤ ↑B + 6) (hbudget : ↑B ≤ delta * (↑(m - nroot).toNat + 1)) (h2gamma : 2 * M.gamma ≤ 1 - alpha) (hK1 : 0 ≤ K1) (hK2 : 0 ≤ K2) (hKhol : 0 ≤ Khol) (hKh : 0 ≤ Kh) (hCosc : 0 ≤ Cosc) (hoscHi : 0 ≤ oscHi) (hoscData : 0 ≤ oscData) (hbrG : (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ ≤ rootClauseBTopKs M.gamma m (n + 3) * (↑(Section3.Annealed.sigmaBar M m))⁻¹) (hDD : stepSevenNuGradNorm M.nu (ExcessDecay.truncatedWindow z m n) uglob.grad ≤ K1 * (3 * (1 + K2) * (√↑(Section3.Annealed.sigmaBar M (n + 3)) * (3 ^ (-(n + 3)) * Support.normalizedL2On (ExcessDecay.truncatedWindow z m (n + 3)) fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m (n + 3)) uglob.toFun)) + stepSevenFlushCG d K2 * (√(↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * (Real.rpow 3 (↑m / 2) * Khol)) + stepSevenFlushCH d K2 * (√↑(Section3.Annealed.sigmaBar M (n + 3)) * (Real.rpow 3 (↑m / 2) * Kh)))) (hosc : (3 ^ (-(n + 3)) * Support.normalizedL2On (ExcessDecay.truncatedWindow z m (n + 3)) fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m (n + 3)) uglob.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha nroot m) * oscHi + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha nroot m) * oscData) : stepSevenNuGradNorm M.nu (ExcessDecay.truncatedWindow z m (nroot + 1)) uglob.grad ≤ stepSevenFlushCg d K1 K2 Cosc * √↑(Section3.Annealed.sigmaBar M (n + 3)) * Real.rpow 3 (3 / 4 * stepSixExponent alpha nroot m) * oscHi + stepSevenFlushCg d K1 K2 Cosc * Real.rpow 3 (3 / 4 * stepSixExponent alpha nroot m) * (√↑(Section3.Annealed.sigmaBar M (n + 3)) * (oscData + Real.rpow 3 (↑m / 2) * Kh) + √(↑(Section3.Annealed.sigmaBar M m))⁻¹ * (Real.rpow 3 (↑m / 2) * Khol))

The flush branch, in the Step-7 chain's hgrad slot.

The unit-D window energy (priced through §3), the Step-6 oscillation bound and the print's volume passage, assembled into the shape StepSevenMean.exists_stepSevenEnd_chain_of_lambda_hmeanFree consumes, at shomNp := σ_{n+3}, dataOsc := oscData + 3^{m/2}K_h and dataM:= √σ_m^{-1}·3^{m/2}·K_g.