StepThreePackage

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

t.regularity Step 3, assembled: one a.e. statement carrying the windows,

the bad-scale budget, the separation, and the ε_j(z) caps

What is delivered

StepThreeWindowsAndBudget states ABK26 t.regularity Step 3 at one window [n, m], uniformly over the printed triadic lattice centres z ∈ 3^n ℤ^d ∩ □_m:

• U_j := (z + □_j) ∩ □_m is an admissible iteration-lemma family (IterationWindowFamily: measurable, nested, sandwiched);
• 𝓑_z ⊆ [n, m], the iteration lemma's B-binder;
• |𝓑_z| ≤ δ(m - n + 1), e.bad.scale.proportion.bound;
• |𝓑_z| + 7 ≤ m - n, the separation.

stepThreeWindowsAndBudget_of_goodScaleWindows produces all four from the producer's good-scales clause alone, at δ ∈ [0, 1/2] and a window of at least 14 scales. This is what the Step-4 excess-decay application and the Step-5 iteration application read off Step 3.

What is not formed here

The excess E_j := E(u, U_j) = 3^{-j} min_ℓ ‖u - ℓ‖_{L²(U_j)} and the optimal affine functions ℓ_j are NOT formed: they are functions of the solution u, which enters only with Step 4's excess-decay lemma, and the development already carries their carriers (Support.affineExcess, Support.IsAffineMinimizer) for the frozen iteration lemma. Step 3's own content — the windows, the bad set, the budget — is what this module delivers. Nothing about u, g, h, L or the truncated operator a_L appears here; the L-reconciliation gap is untouched.

References

• ABK26, t.regularity Steps 1--3.

1. The per-window conclusion

def Algsuperdiff.Section4.Provider.Regularity.StepThreeWindowsAndBudget {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The Step-3 conclusion at one window [n, m], uniformly over the printed lattice centres z ∈ 3^n ℤ^d ∩ □_m: the window family is an admissible iteration family, the bad set sits in the counting window, it obeys e.bad.scale.proportion.bound, and it satisfies the separation.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeWindowsAndBudget_of_goodScaleWindows {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ 1 / 2) (hwin : 14 ≤ m - n) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) : StepThreeWindowsAndBudget M delta n m omega

The per-window conclusion, from the producer's good-scales clause alone.