FreshShellSumZeroDirection

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

The correctors of e.def.w vanish at the zero direction

ABK26, e.def.w.

Step 6 of l.approximate.recurrence.formula#localization reads the Step-4 and Step-5 displays at a single direction: the Dirichlet leg at e = 0 and the Neumann leg at e' = 0. At those branches the manuscript writes the bare direction in the load slot, whereas the formal load (gaugedPrincipalLoadShell) carries direction + (grad w)_R. The two agree because the corresponding forcing -streamForcing c ω n m 0 vanishes identically, so the corrector's gradient vanishes by uniqueness of the weak solution -- FreshShellUniqueness, whose two side conditions (nonempty domain, uniform ellipticity) are already discharged there.

What is supplied

• streamForcing_zero_direction -- the forcing at direction 0 is the zero field.
• isZeroTraceDirichletRhsWeakSolution_one_zero, isMeanZeroNeumannRhsWeakSolution_one_zero -- the zero function solves the zero-forcing problem in both gauges.
• gradToVectorL2_eq_zero_of_isZeroTraceDirichletRhsWeakSolution_streamForcing_zero, gradToVectorL2_eq_zero_of_isMeanZeroNeumannRhsWeakSolution_streamForcing_zero -- the L² gradient of either corrector vanishes at the zero direction.
• grad_ae_eq_zero_of_isZeroTraceDirichletRhsWeakSolution_streamForcing_zero, grad_ae_eq_zero_of_isMeanZeroNeumannRhsWeakSolution_streamForcing_zero -- the pointwise a.e. form, which is what collapses a cube average of the corrector gradient to 0.

No uniqueness hypothesis is introduced: uniqueness is proved upstream and consumed. No normalization, scale gate or model field enters; the statements hold at every triadic cube, every gauge c, every sample and every shell pair.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.streamForcing_zero_direction {d : ℕ} (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) : streamForcing c omega n m 0 = fun (x : HCPolySupport.Vec d) => 0

The fresh-shell forcing at the zero direction is the zero field.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.neg_streamForcing_zero_direction {d : ℕ} (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) : (fun (x : HCPolySupport.Vec d) => -streamForcing c omega n m 0 x) = fun (x : HCPolySupport.Vec d) => 0

The negated forcing at the zero direction is again the zero field.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.isZeroTraceDirichletRhsWeakSolution_one_zero {d : ℕ} (U : Set (HCPolySupport.Vec d)) : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) U 0 fun (x : HCPolySupport.Vec d) => 0

The zero function is a zero-trace Dirichlet weak solution at zero forcing.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.isMeanZeroNeumannRhsWeakSolution_one_zero {d : ℕ} (U : Set (HCPolySupport.Vec d)) : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) U 0 fun (x : HCPolySupport.Vec d) => 0

The zero function is a mean-zero Neumann weak solution at zero forcing.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradToVectorL2_zero_h10 {d : ℕ} (U : Set (HCPolySupport.Vec d)) : (HCPolySupport.H10Function.toH1Function 0).gradToVectorL2 = 0

The L² gradient of the zero H¹₀ function vanishes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradToVectorL2_zero_h1MeanZero {d : ℕ} (U : Set (HCPolySupport.Vec d)) : HCPolySupport.H1MeanZeroFunction.gradToVectorL2 0 = 0

The L² gradient of the zero mean-zero H¹ function vanishes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradToVectorL2_eq_zero_of_isZeroTraceDirichletRhsWeakSolution_streamForcing_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) {w : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)} (hw : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -streamForcing c omega n m 0 x) : w.gradToVectorL2 = 0

The Dirichlet corrector vanishes at the zero direction.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradToVectorL2_eq_zero_of_isMeanZeroNeumannRhsWeakSolution_streamForcing_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) {w : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hw : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -streamForcing c omega n m 0 x) : w.gradToVectorL2 = 0

The Neumann corrector vanishes at the zero direction.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.grad_ae_eq_zero_of_isZeroTraceDirichletRhsWeakSolution_streamForcing_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) {w : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)} (hw : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -streamForcing c omega n m 0 x) : w.grad =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] 0

The pointwise form, Dirichlet leg. This is what collapses a cube average of the corrector gradient to 0.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.grad_ae_eq_zero_of_isMeanZeroNeumannRhsWeakSolution_streamForcing_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) {w : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hw : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -streamForcing c omega n m 0 x) : w.toH1Function.grad =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] 0

The pointwise form, Neumann leg.