RootClauseBInputs #

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

3. at the full cube: the `hgradE` identity #

source

theorem Algsuperdiff.Section4.Provider.Regularity.forcedSolutionEnergyNorm_fluxCorrected_eq_nuGradNorm {d : ℕ} (M : Section3.ABKModel d) (L mf m j : ℤ) (Qf : HCPolySupport.TriadicCube d) {z : HCPolySupport.Vec d} (omega : Section3.Cutoff.CutoffSample d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u : HCPolySupport.Book.Ch03.ForcedCubeSolution (HCPolySupport.originCube d j) (Support.fluxCorrectedCoeffFamily M L mf Qf (Section3.Cutoff.translateCutoffSample z omega)) g) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (hg : ∀ (y : HCPolySupport.Vec d), u.toH1.grad y = G (y + z)) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1))) (hj : j ≤ m - 1) :

HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm (HCPolySupport.originCube d j) (Support.fluxCorrectedCoeffFamily M L mf Qf (Section3.Cutoff.translateCutoffSample z omega)) u = stepSevenNuGradNorm M.nu (ExcessDecay.truncatedWindow z m j) G

proved the ν-identification at the Caccioppoli core □_{j-2} (sqrt_localizedCoeffEnergyValue_core_eq_nuGradNorm); the chain's hgradE slot needs it at openCubeSet □_j, which is the same three-line identity — the symmetric part of the flux-corrected family IS ν I, the frame moves by the translation transport, and the window IS the translate on the interior branch.