Coarse-graining support: Support.Sobolev.PotentialSolenoidalL2Realization

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

Closed-range realization for the canonical zero-trace potential subspace

This file closes the last abstract hypothesis used by the note-facing coarse Poincare theorem surface. The proof combines:

• the representative upgrade exists_h10Function_of_mem_h10GraphClosedSubmodule from Foundations/H10Graph.lean, which shows every point of the closed H¹₀ graph is realized by an honest H¹₀ function, and
• the closed-range gradient projection H10GraphClosed.isClosed_range_gradientCLM.

Together they discharge HasPotentialZeroTraceClosureRealization U on every bounded open convex domain.

theorem HCPolySupport.PotentialSolenoidalL2Data.hasPotentialZeroTraceClosureRealization_of_convexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : HasPotentialZeroTraceClosureRealization U

Main realization theorem: on bounded open convex domains, every member of the canonical closed zero-trace potential subspace is the gradient of an actual H¹₀ function.