RootClauseBCloseAssembly

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

theorem Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBTopPayload {d : ℕ} [NeZero d] {M : Section3.ABKModel d} {m0 : ℤ} {Ecap : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ecap) (hgamma : M.gamma < 1 / 2) {C1 alpha Khol CB Cdel Cosc : ℝ} {n m L : ℤ} {x : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} {uglob : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} (hmerge : ∀ (k n0 : ℤ) (v0 : Fin d → ℤ), omega ∈ stepThreeGoodEvent M (stepOneDelta C1 alpha) 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) (hwin : RootWindowPayload M C1 alpha n m omega) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hzin : offGridCentre n x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1))) (hmL : m ≤ L) (hmm0 : m ≤ m0) (hKhol : 0 ≤ Khol) (hCB : 0 ≤ CB) (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)))) (hosc : ∀ (n' kc : ℤ), n ≤ n' → n' ≤ kc → kc ≤ m → (3 ^ (-n') * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m n') fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (offGridCentre n x) m n') uglob.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (3 ^ (-kc) * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m kc) fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (offGridCentre n x) m kc) uglob.toFun) + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (edFinalDataG M Cdel (Khol * stepFourGagliardoConst d stepOneS) m + 0)) : ∃ (kc : ℤ) (n' : ℤ) (B : ℕ), n' ≤ m - 1 ∧ n + 1 ≤ n' - 2 ∧ n' ≤ kc ∧ kc ≤ m - 1 ∧ m - (kc + 1) ≤ ↑B + 1 ∧ n' - n ≤ ↑B + 6 ∧ ↑B ≤ stepOneDelta C1 alpha * (↑(m - n).toNat + 1) ∧ RootClauseBTopPayload M L Khol (rootClauseBDataBConst d) CB CB Cdel Cosc (rootClauseBDataMConst d CB) alpha n m kc n' x omega uglob gsrc

The clause-(B) payload, produced from the root's own a.e. block.

The two scales, their six side conditions and the Step-7c budget scalar are all chosen and discharged inside.

2. Clause (B) from RootWindowPayload and hosc ALONE

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_display_offGrid_of_windowPayload (d : ℕ) [NeZero d] : ∃ (Cch : ℝ) (Cc : ℝ), 0 < Cch ∧ 0 < Cc ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma < 1 / 2 → ∀ (L : ℤ) {C1 alpha : ℝ} {n m : ℤ} {x : HCPolySupport.Vec d} (omega : Section3.Cutoff.CutoffSample d) (uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {Khol CB Cdel Cosc Cest : ℝ}, m ≤ m0 → n ≤ m → m ≤ L → (∀ (k n0 : ℤ) (v0 : Fin d → ℤ), omega ∈ stepThreeGoodEvent M (stepOneDelta C1 alpha) 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) → RootWindowPayload M C1 alpha n m omega → x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → offGridCentre n x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) uglob hdat gsrc → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Khol gsrc → 0 ≤ Khol → 0 ≤ CB → 0 ≤ Cdel → 0 ≤ Cosc → 2 * ↑d + 2 ≤ C1 → 0 ≤ alpha → alpha ≤ 1 → (∀ (n' kc : ℤ), n ≤ n' → n' ≤ kc → kc ≤ m → (3 ^ (-n') * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m n') fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (offGridCentre n x) m n') uglob.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (3 ^ (-kc) * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m kc) fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (offGridCentre n x) m kc) uglob.toFun) + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (edFinalDataG M Cdel (Khol * stepFourGagliardoConst d stepOneS) m + 0)) → rootClauseBPrefactor d Cch (rootClauseBCaccUniform Cc CB) Cosc CB CB (rootClauseBTopCtr d (rootClauseBDataBConst d)) (edFinalDataOscW M Cdel * stepFourGagliardoConst d stepOneS) (rootClauseBDataMConst d CB) ≤ Cest → offGridCentre n x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → (√M.nu * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m (n + 1)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (uglob.grad y))) ≤ Cest * Real.rpow 3 ((1 - alpha) * (↑m - ↑n)) * ((√M.nu * Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (uglob.grad y))) + √(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Khol)

The clause-(B) endpoint at the root's own inputs.

The second conjunct of RootAssemblyConditional.RootLatticeDisplay, produced from: the root's own a.e. block RootWindowPayload; the merged A6 clause-(B) record; the frozen Section-3 inductionState; the root's own Dirichlet datum and its printed C^{0,1/2} binder on 𝐠; hosc; and the ω-free funding line. No scale is caller data and no MemLp is caller data — both are produced inside.