RootClauseBCloseCaps

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

1. The merged clause-(B) record

theorem Algsuperdiff.Section4.Provider.Regularity.ae_stepSevenLambdaCaps_merged (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ delta ∈ Set.Ioc 0 (1 / 2), 8 * M.gamma ≤ stepOneSEighth → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp delta → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (k n : ℤ) (v : Fin d → ℤ), omega ∈ stepThreeGoodEvent M delta k (Support.triadicLatticePoint n v) → ∀ (L : ℤ), k ≤ L → StepSevenLambdaCaps (HCPolySupport.originCube d k) (Support.fluxCorrectedCoeffFamily M L k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n v) omega)) (↑(Section3.Annealed.sigmaBar M k)) (2 * ↑d * ((C * stepOneEp delta) ^ 2 + 1))

ae_stepSevenLambdaCaps with the scale AND the printed centre inside the almost-everywhere quantifier.

One null set serves every scale k : ℤ and every printed lattice centre Support.triadicLatticePoint n v; the index set ℤ × ℤ × (Fin d → ℤ) is countable, so this is Mathlib's ae_all_iff and nothing more.

2. The clause-(B) record at BOTH selected scales

theorem Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBCapsPair {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m L : ℤ} {omega : Section3.Cutoff.CutoffSample d} {CB : ℝ} (hmerge : ∀ (k n0 : ℤ) (v0 : Fin d → ℤ), omega ∈ stepThreeGoodEvent M delta k (Support.triadicLatticePoint n0 v0) → ∀ (L' : ℤ), k ≤ L' → StepSevenLambdaCaps (HCPolySupport.originCube d k) (Support.fluxCorrectedCoeffFamily M L' k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n0 v0) omega)) (↑(Section3.Annealed.sigmaBar M k)) CB) (hbudget : StepThreeWindowsAndBudget M delta n m omega) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) (hmL : m ≤ L) : ∃ (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 ∧ StepSevenLambdaCaps (HCPolySupport.originCube d j) (Support.fluxCorrectedCoeffFamily M L j (HCPolySupport.originCube d j) (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n v) omega)) (↑(Section3.Annealed.sigmaBar M j)) CB ∧ StepSevenLambdaCaps (HCPolySupport.originCube d k) (Support.fluxCorrectedCoeffFamily M L k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n v) omega)) (↑(Section3.Annealed.sigmaBar M k)) CB

The two clause-(B) records the chain consumes, produced.

RootClauseBCloseSelection's joint pigeonhole selects the two good scales j ≤ k from the separation |𝓑| + 7 ≤ m - n; the merged record then supplies the clause-(B) data at both. The caps field of the payload sits at □_k (the chain's coarse cube □_{k_c+1} at k_c = k-1) and capsCacc at □_j (the Caccioppoli's cube □_{n'+1} at n' = j-1).