RootClauseBCloseSelection

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

1. The candidate range and its good scales

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

The joint candidate range [n+4, m-1] ∩ ℤ: the printed Step-7a range widened at the top to the bad set's own domain, so that a good scale as close to m as the bad set allows is available.

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBCandidates n m = Finset.Icc (n + 4) (m - 1)

theorem Algsuperdiff.Section4.Provider.Regularity.card_rootClauseBCandidates (n m : ℤ) : (rootClauseBCandidates n m).card = (m - n - 4).toNat

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

The good scales of the joint candidate range.

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBGoodScales B n m = Algsuperdiff.Section4.Provider.Regularity.rootClauseBCandidates n m \ B

theorem Algsuperdiff.Section4.Provider.Regularity.mem_rootClauseBGoodScales_iff {B : Finset ℤ} {n m j : ℤ} : j ∈ rootClauseBGoodScales B n m ↔ (n + 4 ≤ j ∧ j ≤ m - 1) ∧ j ∉ B

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBGoodScales_nonempty {B : Finset ℤ} {n m : ℤ} (hsep : ↑B.card + 7 ≤ m - n) : (rootClauseBGoodScales B n m).Nonempty

Non-emptiness under the separation |𝓑| + 7 ≤ m - n; the range has m-n-4 candidates, so |𝓑| + 5 ≤ m - n would already do.

2. The two extrema, with their sharp gaps

theorem Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBGoodPair {B : Finset ℤ} {n m : ℤ} (hsep : ↑B.card + 7 ≤ m - n) : ∃ (j : ℤ) (k : ℤ), n + 4 ≤ j ∧ j ≤ k ∧ k ≤ m - 1 ∧ j ∉ B ∧ k ∉ B ∧ j - n ≤ ↑B.card + 4 ∧ m - k ≤ ↑B.card + 1

The joint good pair.

From the proved separation alone: two good scales j ≤ k inside [n+4, m-1], the lower one within |𝓑| + 4 of the bottom and the upper one within |𝓑| + 1 of the top. They are the minimum and the maximum of the SAME good-scale set, so j ≤ k needs no argument beyond Finset.min'_le_max'.

3. The Step-3 instantiation: both good

theorem Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBCapScales {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) : ∃ (j : ℤ) (k : ℤ), n + 4 ≤ j ∧ j ≤ k ∧ k ≤ m - 1 ∧ j - n ≤ ↑(stepThreeBadSet M delta n m (Support.triadicLatticePoint n v) omega).card + 4 ∧ m - k ≤ ↑(stepThreeBadSet M delta n m (Support.triadicLatticePoint n v) omega).card + 1 ∧ omega ∈ stepThreeGoodEvent M delta j (Support.triadicLatticePoint n v) ∧ omega ∈ stepThreeGoodEvent M delta k (Support.triadicLatticePoint n v)

The two cap scales of the clause-(B) chain, at the Step-3 bad set.

At every printed lattice centre z's StepThreeWindowsAndBudget delivers the separation, and the joint pigeonhole turns it into two scales j ≤ k whose GOOD membership holds at ω — exactly the gate of StepSevenLambdaGoodEvent.ae_stepSevenLambdaCaps at j and at k. Setting the chain's free scales to n' := j - 1 (the Caccioppoli leg) and `k_chain:= k

• 1` (the coarse-graining leg) puts BOTH clause-(B) records on produced cubes.