RootClauseBCoarseFrameWellPlaced

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

1. The two printed inclusions, with no geometry binder

theorem Algsuperdiff.Section4.Provider.Regularity.coarseFrame_subset_openCubeSet {d : ℕ} {m k : ℤ} (z : HCPolySupport.Vec d) (hkm : k ≤ m) : (fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The printed sandwich, upper half. The well-placed coarse cube lies in □_m for every centre, at the single scale comparison k ≤ m. A restatement of BoundaryCoveringGeometry.image_add_wellPlacedCentre_subset_openCubeSet under the name the Step-7 chain reads.

theorem Algsuperdiff.Section4.Provider.Regularity.truncatedWindow_subset_coarseFrame {d : ℕ} {m k : ℤ} (z : HCPolySupport.Vec d) (hkm : k ≤ m) : ExcessDecay.truncatedWindow z m k ⊆ (fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)

The printed sandwich, lower half. The Step-7 chain's coarse-window inclusion truncatedWindow z m k ⊆ c + □_k, at no geometry binder.

theorem Algsuperdiff.Section4.Provider.Regularity.volume_coarseFrame_ne_top {d : ℕ} {m k : ℤ} (z : HCPolySupport.Vec d) (hkm : k ≤ m) : MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) ≠ ⊤

The well-placed coarse cube has finite volume.

2. The five IntegrableOn slots at the well-placed cube

theorem Algsuperdiff.Section4.Provider.Regularity.integrableOn_truncatedWindow_pack {d : ℕ} {m k : ℤ} (z : HCPolySupport.Vec d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : MeasureTheory.IntegrableOn u.toFun (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u.toFun x ^ 2) (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume

The chain's two window integrability slots, at no geometry binder.

theorem Algsuperdiff.Section4.Provider.Regularity.integrableOn_coarseFrame_pack {d : ℕ} {m k : ℤ} (z : HCPolySupport.Vec d) (hkm : k ≤ m) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (b : ℝ) : MeasureTheory.IntegrableOn u.toFun ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u.toFun x ^ 2) ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (u.toFun x - b) ^ 2) ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume

The chain's three covering-cube integrability slots, at no geometry binder.

5. The force's Besov regularity and the dataB leg at the well-placed cube

theorem Algsuperdiff.Section4.Provider.Regularity.forceBesovRegularity_coarseFrame {d : ℕ} [NeZero d] {m k : ℤ} {z : HCPolySupport.Vec d} {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} (hkm : k ≤ m) (hgL2 : MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hgW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d k) stepOneS fun (x : HCPolySupport.Vec d) => -gsrc (x + ExcessDecay.wellPlacedCentre z m k)

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_dataB_coarseFrame {d : ℕ} [NeZero d] {m k : ℤ} {z : HCPolySupport.Vec d} {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {Khol : ℝ} (hkm : k ≤ m) (hKhol : 0 ≤ Khol) (hgHol : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Khol gsrc) (hgL2 : MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hgW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d k) stepSevenCgS fun (y : HCPolySupport.Vec d) => -gsrc (y + ExcessDecay.wellPlacedCentre z m k)) ≤ rootClauseBDataBConst d * edFinalDataOscG Khol m

The dataB leg at the print's own coarse frame, at no geometry binder.

RootClauseBGateGeometry.rootClauseB_dataB_gate at z:= wellPlacedCentre z m k. The printed 3^{k/2} ≤ 3^{m/2} step is the same scale comparison k ≤ m that discharges the gate, so the statement carries exactly one integer hypothesis.