StepThreeBudget

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

t.regularity Step 3: the bad-scale budget, centre-uniformly, and the

separation |𝓑_z| + 7 ≤ m - n

The target

ABK26 e.bad.scale.proportion.bound:

|𝓑_z| ≤ max_{z' ∈ 3^n ℤ^d ∩ □_m} Σ_{j=n}^{m} (1 - 1_{𝒢(j,z'; ⅛s, ⅛ s δ^{1/2})})
      ≤ δ (m - n + 1) = C₁^{-1}(1-α)(m-n+1) .

The producer is the Algsuperdiff.Frozen.Section4.minimal_scale_separation whose conclusion body exported as GoodScaleWindows: its S clause is literally the centre-uniform Cesàro density

sup_{z' ∈ 3^{n-1} ℤ^d ∩ □_m} ( (m-n+1)^{-1} Σ_{k=n}^{m} 1_{𝒢(k,z')ᶜ} ) ≤ δ ,

Multiplying the Cesàro form by (m-n+1) and dropping the scale m (which 𝓑_z does not contain) is the whole conversion.

The producer's lattice is finer than the printed one

The producer's supremum runs over 3^{n-1} ℤ^d ∩ □_m, the printed maximum over 3^{n} ℤ^d ∩ □_m. Since 3^n ℤ^d ⊆ 3^{n-1} ℤ^d (triadicLatticePoint_shift), the delivered bound is at least as strong as the printed one at every printed centre; stepThreeBadSet_card_le_of_goodScaleWindows is the printed statement, ..._fine the stronger one actually available.

The separation |𝓑_z| + 7 ≤ m - n, resolved

The honest resolution, with the exact arithmetic:

• the budget is |𝓑| ≤ δ(t+1) with t := m - n, and δ ≤ 1/2 (stepOneDelta_mem), so 2|𝓑| ≤ t + 1;
• |𝓑| is an integer, so this is |𝓑| ≤ ⌊(t+1)/2⌋, and ⌊(t+1)/2⌋ + 7 ≤ t holds iff t ≥ 14 — for even t at t ≥ 14 (t/2 + 7 ≤ t), for odd t at t ≥ 15 ((t+1)/2 + 7 ≤ t), and t = 15 is the first odd value. The naive real-valued reading (t+1)/2 + 7 ≤ t ↔ t ≥ 15 is one unit pessimistic; integrality buys the missing unit at t = 14;
• t = 13 genuinely fails (|𝓑| ≤ 7 and 7 + 7 = 14 > 13), so a window length of 13 does not suffice;
• the fix costs nothing: X_m(α) = Z_m + k + 3 ≥ 14 needs only k ≥ 11, and k = ⌈4 log₃(16 C_edos)⌉ ≥ 11 follows from the same explicit floor 1 ≤ C_edos that gives k ≥ 10 — because ⌈x⌉ ≥ 11 ↔ x > 10 and 3^5 = 243 < 256 = 16² is a strict inequality. So no C_edos floor moves, no k-formula moves, and no statement anywhere changes; only the pin sharpens from k ≥ 10, X ≥ 13 to k ≥ 11, X ≥ 14.

The exact C_edos floor for k ≥ 11 is C_edos > 3^{5/2}/16 = 0.97427…, so the standing floor C_edos ≥ 1 has room; the floor for k ≥ 12 would be C_edos > 3^{11/4}/16 = 1.28…, which is not free, and is not needed.

Contents

• triadicLatticePoint_shift, mem_latticeCubeSet_shift, mem_openCubeSet_of_mem_latticeCubeSet — the lattice bookkeeping.
• stepThreeBadSet_card_le_of_goodScaleWindows(_fine) — the budget.
• fourteen_le_minimalScaleX, fourteen_le_window — the sharpened window-length pin.
• stepOneBadSetSeparation_of_card_le, stepOneBadSetSeparation_of_goodScaleWindows — the separation.

References

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

1. The lattice bookkeeping

theorem Algsuperdiff.Section4.Provider.Regularity.triadicLatticePoint_shift {d : ℕ} (n : ℤ) (v : Fin d → ℤ) : (Support.triadicLatticePoint (n - 1) fun (i : Fin d) => 3 * v i) = Support.triadicLatticePoint n v

3^n v = 3^{n-1}(3v): the printed centre lattice 3^n ℤ^d sits inside the producer's finer lattice 3^{n-1} ℤ^d.

theorem Algsuperdiff.Section4.Provider.Regularity.mem_latticeCubeSet_shift {d : ℕ} {n m : ℤ} {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : (fun (i : Fin d) => 3 * v i) ∈ Support.latticeCubeSet d (n - 1) m

The embedding on index sets.

theorem Algsuperdiff.Section4.Provider.Regularity.mem_openCubeSet_of_mem_latticeCubeSet {d : ℕ} {n m : ℤ} {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : Support.triadicLatticePoint n v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

A lattice centre of 3^n ℤ^d ∩ □_m lies in □_m — the hypothesis the window family's sandwich needs.

2. The budget

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet_card_le_of_goodScaleWindows_fine {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta : 0 ≤ delta) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {w : Fin d → ℤ} (hw : w ∈ Support.latticeCubeSet d (n - 1) m) : ↑(stepThreeBadSet M delta n m (Support.triadicLatticePoint (n - 1) w) omega).card ≤ delta * (↑(m - n).toNat + 1)

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet_card_le_of_goodScaleWindows {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta : 0 ≤ delta) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : ↑(stepThreeBadSet M delta n m (Support.triadicLatticePoint n v) omega).card ≤ delta * (↑(m - n).toNat + 1)

e.bad.scale.proportion.bound, at the printed centres z ∈ 3^n ℤ^d ∩ □_m and uniformly in them:

|𝓑_z| ≤ δ (m - n + 1) .

3. The sharpened window-length pin

theorem Algsuperdiff.Section4.Provider.Regularity.fourteen_le_minimalScaleX {Omega : Type u_1} (Z : Omega → ℕ∞) {k : ℕ} (hk : 11 ≤ k) (omega : Omega) : 14 ≤ minimalScaleX Z k omega

X_m(α) ≥ 14 at k ≥ 11 (the sharpened pin).

theorem Algsuperdiff.Section4.Provider.Regularity.fourteen_le_window {Omega : Type u_1} (Z : Omega → ℕ∞) {k : ℕ} (hk : 11 ≤ k) (omega : Omega) {n m : ℤ} (hgate : minimalScaleX Z k omega ≤ ↑(m - n).toNat) : 14 ≤ m - n

The window-length demand of Step 3: at k ≥ 11, the gate X_m(α) ≤ m - n is available only on windows of length at least 14 — the length the separation needs.

4. The separation

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneBadSetSeparation_of_card_le {c : ℕ} {delta : ℝ} {n m : ℤ} (hdelta : delta ≤ 1 / 2) (hwin : 14 ≤ m - n) (hcard : ↑c ≤ delta * (↑(m - n).toNat + 1)) : StepOneBadSetSeparation c n m

The separation, from the budget: at δ ≤ 1/2 and window length at least 14, |𝓑| + 7 ≤ m - n. The integrality of |𝓑| is what makes 14 (rather than 15) the threshold.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneBadSetSeparation_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) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : StepOneBadSetSeparation (stepThreeBadSet M delta n m (Support.triadicLatticePoint n v) omega).card n m