StepSevenGoodScales

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

t.regularity Step 7a: the extreme good scales n', m'

The target

  n' := min { j ∈ [n+3, m-3] ∩ ℤ : j ∉ 𝓑 } ,
  m' := max { j ∈ [n+3, m-3] ∩ ℤ : j ∉ 𝓑 } ,
  max{ n' - n , m - m' } ≤ |𝓑| + 6 .

This module supplies them.

What is delivered

• StepSevenSelection B n m n' m' — the selection as a named proposition: the two range facts, the two goodness facts, and the two facts (n' minimal, m' maximal among the good scales of [n+3, m-3]). The extremality form is what the gaps are proved from, so no consumer has to re-run a min/max.
• StepSevenSelection.lower_gap / upper_gap — n' - n ≤ |𝓑| + 3 and m - m' ≤ |𝓑| + 3, the sharp gaps; max_gap_le is the printed max{n'-n, m-m'} ≤ |𝓑| + 6. (The consumer asks for m - m' ≤ |𝓑| + 3, i.e. the sharp form, so both are exported.)
• the Step-3 instantiation: exists_stepSevenSelection_stepThreeBadSet at 𝓑 = stepThreeBadSet, and mem_stepThreeGoodEvent_of_stepSevenSelection, which turns "n' is a good scale" into the good-event membership ω ∈ 𝒢(n', z; ⅛s, ⅛ s δ^{1/2}) that Step 7b (l.lambdas.stability) consumes.

The two combinatorial arguments, in one line each

Non-emptiness: #(Icc (n+3) (m-3)) = m - n - 5 and #(Icc (n+3) (m-3)) ≤ #(Icc (n+3) (m-3) \ 𝓑) + #𝓑, so |𝓑| + 6 ≤ m - n forces the difference to be non-empty.

The gaps: minimality of n' puts the whole interval [n+3, n'-1] inside 𝓑, and that interval has n' - n - 3 elements; symmetrically (m', m-3] has m - m' - 3 elements. Both gaps are therefore ≤ |𝓑| + 3.

References

• ABK26, t.regularity Step 7.

1. The candidate index set

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenCandidates (n m : ℤ) : Finset ℤ

The Step-7a candidate range [n+3, m-3] ∩ ℤ.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenCandidates n m = Finset.Icc (n + 3) (m - 3)

theorem Algsuperdiff.Section4.Provider.Regularity.card_stepSevenCandidates (n m : ℤ) : (stepSevenCandidates n m).card = (m - n - 5).toNat

The candidate range has m - n - 5 elements.

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenGoodScales (B : Finset ℤ) (n m : ℤ) : Finset ℤ

The good scales of the Step-7a range: the candidates outside the bad set.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenGoodScales B n m = Algsuperdiff.Section4.Provider.Regularity.stepSevenCandidates n m \ B

theorem Algsuperdiff.Section4.Provider.Regularity.mem_stepSevenGoodScales_iff {B : Finset ℤ} {n m j : ℤ} : j ∈ stepSevenGoodScales B n m ↔ (n + 3 ≤ j ∧ j ≤ m - 3) ∧ j ∉ B

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenGoodScales_nonempty {B : Finset ℤ} {n m : ℤ} (hsep : ↑B.card + 6 ≤ m - n) : (stepSevenGoodScales B n m).Nonempty

2. The selection, as a named proposition

structure Algsuperdiff.Section4.Provider.Regularity.StepSevenSelection (B : Finset ℤ) (n m n' m' : ℤ) : Prop

The Step-7a selection: n' is the smallest and m' the largest good scale of [n+3, m-3]. The two extremality clauses are stated as universally quantified minimality/maximality, which is what the gap bounds are proved from, so a consumer never has to re-run the min/max.

• lower_lo : n + 3 ≤ n'

  n+3 ≤ n'.

• lower_hi : n' ≤ m - 3

  n' ≤ m-3.

• upper_lo : n + 3 ≤ m'

  n+3 ≤ m'.

• upper_hi : m' ≤ m - 3

  m' ≤ m-3.

• lower_good : n' ∉ B

  n' is a good scale.

• upper_good : m' ∉ B

  m' is a good scale.

• lower_min (j : ℤ) : n + 3 ≤ j → j ≤ m - 3 → j ∉ B → n' ≤ j

  n' is the smallest good scale of the range.

• upper_max (j : ℤ) : n + 3 ≤ j → j ≤ m - 3 → j ∉ B → j ≤ m'

  m' is the largest good scale of the range.

theorem Algsuperdiff.Section4.Provider.Regularity.StepSevenSelection.le {B : Finset ℤ} {n m n' m' : ℤ} (h : StepSevenSelection B n m n' m') : n' ≤ m'

n' ≤ m'.

theorem Algsuperdiff.Section4.Provider.Regularity.StepSevenSelection.lower_gap {B : Finset ℤ} {n m n' m' : ℤ} (h : StepSevenSelection B n m n' m') : n' - n ≤ ↑B.card + 3

The sharp lower gap n' - n ≤ |𝓑| + 3: minimality of n' puts the whole interval [n+3, n'-1] — which has n' - n - 3 elements — inside 𝓑.

theorem Algsuperdiff.Section4.Provider.Regularity.StepSevenSelection.upper_gap {B : Finset ℤ} {n m n' m' : ℤ} (h : StepSevenSelection B n m n' m') : m - m' ≤ ↑B.card + 3

The sharp upper gap m - m' ≤ |𝓑| + 3 — the form the consumer asks for.

theorem Algsuperdiff.Section4.Provider.Regularity.StepSevenSelection.max_gap_le {B : Finset ℤ} {n m n' m' : ℤ} (h : StepSevenSelection B n m n' m') : max (n' - n) (m - m') ≤ ↑B.card + 6

The printed observation: max{ n' - n, m - m' } ≤ |𝓑| + 6.

theorem Algsuperdiff.Section4.Provider.Regularity.StepSevenSelection.lt {B : Finset ℤ} {n m n' m' : ℤ} (h : StepSevenSelection B n m n' m') (hsep : ↑B.card + 7 ≤ m - n) : n' < m'

The pigeonhole: if m' ≤ n' then extremality forces every good scale of [n+3, m-3] to equal n', so all m - n - 6 other candidates are bad.

3. The witnesses

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenSelection {B : Finset ℤ} {n m : ℤ} (hsep : ↑B.card + 6 ≤ m - n) : ∃ (n' : ℤ) (m' : ℤ), StepSevenSelection B n m n' m'

The Step-7a selection exists, as soon as the printed window demand |𝓑| + 6 ≤ m - n holds. The witnesses are literally the manuscript's min and max over the good scales of [n+3, m-3].

4. The Step-3 instantiation

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenSelection_stepThreeBadSet {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {z : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} (hsep : StepOneBadSetSeparation (stepThreeBadSet M delta n m z omega).card n m) : ∃ (n' : ℤ) (m' : ℤ), StepSevenSelection (stepThreeBadSet M delta n m z omega) n m n' m' ∧ n' < m'

The selection at the Step-3 bad set 𝓑_z's separation StepOneBadSetSeparation (|𝓑_z| + 7 ≤ m - n) — which supplies both the printed demand +6 and the extra unit, so n' < m' comes for free.

theorem Algsuperdiff.Section4.Provider.Regularity.mem_stepThreeGoodEvent_of_notMem_stepThreeBadSet {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m j : ℤ} {z : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} (hlo : n ≤ j) (hhi : j ≤ m - 1) (hj : j ∉ stepThreeBadSet M delta n m z omega) : omega ∈ stepThreeGoodEvent M delta j z

A selected scale IS a good scale of Step 3: j ∉ 𝓑_z together with n ≤ j ≤ m-1 is exactly ω ∈ 𝒢(j, z; ⅛s, ⅛ s δ^{1/2}), the good event l.lambdas.stability (Step 7b) is applied on.

theorem Algsuperdiff.Section4.Provider.Regularity.mem_stepThreeGoodEvent_of_stepSevenSelection {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m n' m' : ℤ} {z : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} (h : StepSevenSelection (stepThreeBadSet M delta n m z omega) n m n' m') : omega ∈ stepThreeGoodEvent M delta n' z ∧ omega ∈ stepThreeGoodEvent M delta m' z

The good event at the two selected scales, packaged. The range facts n ≤ n', m' ≤ m - 1 are read off the selection's own [n+3, m-3] range.