Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentH1

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Parent-cube H¹ reflection handoff

The all-face coordinate-fold reflection is recovered as an honest parent-cube H1Function by proving that its scalar/vector representatives lie in the closed weak-gradient graph on the parent cube.

theorem HCPolySupport.exists_cubeFaceReflectionParentH1Function_originCube {d : ℕ} {m : ℤ} (u : H1Function (openCubeSet (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) u.toFun ∧ uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.grad y

The all-face coordinate-fold reflection on centered cubes is an honest H¹ function on the centered parent cube.

theorem HCPolySupport.exists_cubeFaceReflectionParentH1Function_grad_originCube {d : ℕ} {m : ℤ} (u : H1Function (openCubeSet (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.grad y

The gradient-only form consumed by the folded-solenoidal Hodge reduction.

theorem HCPolySupport.cubeFaceReflectionParent_reflected_h1_tests_originCube {d : ℕ} {m : ℤ} (φ : H1Function (openCubeSet (originCube d m))) : ∃ (ψ : H1Function (openCubeSet (originCube d (m + 1)))), ψ.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => φ.grad y

The exact reflected-test constructor required by ReflectionParentOrthogonality.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_weakPoissonEquationOn_originCube {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeCoordinateFoldReflectedScalar (originCube d m) F)

Parent reflected weak equation obtained from the isolated H¹ reflection gluing input and the already-proved folded-Hodge bookkeeping.