RootPayloadPrefix

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

1. Item (f): the toNat cast bridge, named

theorem Algsuperdiff.Section4.Provider.Regularity.toNat_sub_cast_real {m n : ℤ} (h : n ≤ m) : ↑(m - n).toNat = ↑m - ↑n

The toNat cast bridge. For n ≤ m, the real cast of the natural window length is the real difference.

3. Item (d): the affine-minimizer family on the Step-3 windows

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepThreeWindow_affineMinimizerFamily {d : ℕ} {m : ℤ} {z : HCPolySupport.Vec d} (hzm : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : ∃ (c : ℤ → ℝ) (slope : ℤ → HCPolySupport.Vec d), ∀ j ≤ m, Support.IsAffineMinimizer (stepThreeWindow z m j) u.toFun (c j) (slope j)

Item (d), proved: the affine-minimizer family exists.

Every Step-4/6 producer binds a pair (c, slope) : (ℤ → ℝ) × (ℤ → Vec d) minimizing the affine distance on stepThreeWindow z m j for all j ≤ m. The family is built scale by scale from the proved ExcessDecay.exists_isAffineMinimizer_truncatedWindow — stepThreeWindow IS truncatedWindow by definition — with the H¹ datum's own L² membership restricted to the window.