StepSevenSelectionPackage

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

t.regularity Step 7a, assembled: the good-scale selection package

What is delivered

StepSevenSelectionData collects, at a fixed printed centre z ∈ 3^n ℤ^d ∩ □_m and a fixed sample ω, everything ABK26 t.regularity Step 7 produces before the first analytic estimate:

• the two extreme good scales n', m' of [n+3, m-3], with n' < m';
• their proximity to the window ends — the sharp n' - n ≤ |𝓑_z| + 3, m - m' ≤ |𝓑_z| + 3 and the printed max{n'-n, m-m'} ≤ |𝓑_z| + 6;
• the good-event memberships ω ∈ 𝒢(n', z; ⅛s, ⅛ s δ^{1/2}) and ω ∈ 𝒢(m', z; ⅛s, ⅛ s δ^{1/2}) — the indicator Step 7b (l.lambdas.stability) is applied against;
• the sandwich centres z', z'' ∈ □_m with, for (y',k') ranging over {(z',m'), (z'',n')}, (z + □_{k'-1}) ∩ □_m ⊆ y' + □_{k'-1} ⊆ (z + □_{k'}) ∩ □_m.

exists_stepSevenSelectionData_of_stepThreeWindowsAndBudget builds the package at a printed centre from the Step-3 window/budget conclusion alone, so the selection is a drop-in successor of the Step-3 endpoint.

What is not here

Nothing analytic. No λ/Λ transport (Step 7b), no coarse-grained Caccioppoli (Step 7c), no σ comparison, no volume factor. In particular the package makes no claim about the window (z + □_{m'-1}) ∩ □_m beyond the inclusions above; the one-scale-below reading of the Step-7 oscillation endpoint is a Step-7c matter and is only enabled here (by n' < m', which puts m'-1 in [n', m']).

References

• ABK26, t.regularity Step 7.

1. The package

structure Algsuperdiff.Section4.Provider.Regularity.StepSevenSelectionData {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (n' m' : ℤ) (zp zpp : HCPolySupport.Vec d) : Prop

The Step-7a selection package at one centre and one sample. See the module docstring for the six items.

• selection : StepSevenSelection (stepThreeBadSet M delta n m z omega) n m n' m'

  n' and m' are the extreme good scales of [n+3, m-3].

• scales_lt : n' < m'

  n' < m', the side condition.

• lower_gap : n' - n ≤ ↑(stepThreeBadSet M delta n m z omega).card + 3

  The sharp lower gap.

• upper_gap : m - m' ≤ ↑(stepThreeBadSet M delta n m z omega).card + 3

  The sharp upper gap (the form consumes).

• max_gap : max (n' - n) (m - m') ≤ ↑(stepThreeBadSet M delta n m z omega).card + 6

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

• good_lower : omega ∈ stepThreeGoodEvent M delta n' z

  The good event at the lower selected scale.

• good_upper : omega ∈ stepThreeGoodEvent M delta m' z

  The good event at the upper selected scale.

• upper_centre_mem : zp ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

  z' ∈ □_m.

• lower_centre_mem : zpp ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

  z'' ∈ □_m.

• upper_sandwich_in : ExcessDecay.truncatedWindow z m (m' - 1) ⊆ (fun (v : HCPolySupport.Vec d) => zp + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (m' - 1))

  (z + □_{m'-1}) ∩ □_m ⊆ z' + □_{m'-1}.

• upper_sandwich_out : (fun (v : HCPolySupport.Vec d) => zp + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (m' - 1)) ⊆ ExcessDecay.truncatedWindow z m m'

  z' + □_{m'-1} ⊆ (z + □_{m'}) ∩ □_m.

• lower_sandwich_in : ExcessDecay.truncatedWindow z m (n' - 1) ⊆ (fun (v : HCPolySupport.Vec d) => zpp + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n' - 1))

  (z + □_{n'-1}) ∩ □_m ⊆ z'' + □_{n'-1}.

• lower_sandwich_out : (fun (v : HCPolySupport.Vec d) => zpp + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n' - 1)) ⊆ ExcessDecay.truncatedWindow z m n'

  z'' + □_{n'-1} ⊆ (z + □_{n'}) ∩ □_m.

2. The package from the centre condition and the separation

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenSelectionData {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {z : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hsep : StepOneBadSetSeparation (stepThreeBadSet M delta n m z omega).card n m) : ∃ (n' : ℤ) (m' : ℤ) (zp : HCPolySupport.Vec d) (zpp : HCPolySupport.Vec d), StepSevenSelectionData M delta n m z omega n' m' zp zpp

Step 7a at one centre: the whole package from z ∈ □_m's separation `|𝓑_z|

• 7 ≤ m - n. The scale conditions n' - 1 ≤ m, m' - 1 ≤ mthe sandwich needs come from the selection's own range[n+3, m-3]`.

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenSelectionData_of_stepThreeWindowsAndBudget {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hbudget : StepThreeWindowsAndBudget M delta n m omega) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : ∃ (n' : ℤ) (m' : ℤ) (zp : HCPolySupport.Vec d) (zpp : HCPolySupport.Vec d), StepSevenSelectionData M delta n m (Support.triadicLatticePoint n v) omega n' m' zp zpp

Step 7a at every printed centre, straight's per-window conclusion StepThreeWindowsAndBudget (whose fourth component IS the separation).