Coarse-graining support: Support.Sobolev.Foundations.Hodge

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

This file isolates the foundational theorem surface for Hodge-style converse statements and basic restriction lemmas.

The restriction theorem is proved directly from the current H1 witness API. The converse theorem is now proved axiom-free from the coercive mean-zero H¹ Hilbert layer: solve the weak gradient problem on the closed graph, kill the orthogonal residual in L², and replace the weak gradient by the original field. The HasHodgeConverse class remains as packaged theorem data for downstream consumers that prefer typeclass style.

class HCPolySupport.HasHodgeConverse {d : ℕ} (U : Set (Vec d)) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Prop

Explicit data for the Hodge-style converse on a domain U.

This keeps the theorem surface available for upstream consumers without hiding a missing proof behind a placeholder. A future analytic sublayer should provide canonical instances by proving the required orthogonal-complement statement.

• isPotentialOn_of_orthogonal_to_solenoidalZeroNormalTrace_of_memVectorL2 {f : Vec d → Vec d} : MemVectorL2 U f → (∀ {g : Vec d → Vec d}, MemVectorL2 U g → IsSolenoidalZeroNormalTraceOn U g → ∫ (x : Vec d) in U, vecDot (g x) (f x) = 0) → IsPotentialOn U f

def HCPolySupport.HodgeConverseCriterion {d : ℕ} (U : Set (Vec d)) : Prop

Explicit orthogonality criterion underlying the Hodge-style converse on U.

This theorem-shaped predicate is the direct non-typeclass entry point for the current development. HasHodgeConverse packages the same statement as an instance when downstream APIs prefer typeclass style.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HasHodgeConverse.hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] [HasHodgeConverse U] : HodgeConverseCriterion U

theorem HCPolySupport.hasHodgeConverse_of_orthogonal_criterion {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : HodgeConverseCriterion U) : HasHodgeConverse U

Package an explicit orthogonality criterion as HasHodgeConverse data.

This is the canonical constructor surface for future analytic work that proves the converse theorem from closed-range or orthogonal-complement arguments.

theorem HCPolySupport.hodgeConverseCriterion_of_h1CoerciveEstimate {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) : HodgeConverseCriterion U

The Hodge-style converse follows from the coercive mean-zero H¹ layer.

This is the first axiom-free theorem surface for the converse inside the repository: solve the weak gradient problem on the coercive Hilbert graph, show the residual is solenoidal with zero normal trace, use the orthogonality hypothesis to kill that residual in L², and then replace the weak gradient by the original field f.

theorem HCPolySupport.hasHodgeConverse_of_h1CoerciveEstimate {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) : HasHodgeConverse U

Package the coercive-Hilbert proof of the Hodge converse as HasHodgeConverse data.

theorem HCPolySupport.hodgeConverseCriterion_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) : HodgeConverseCriterion U

A bounded open convex domain satisfies the Hodge converse once the direct mean-zero L² Poincare theorem is available on the H¹ layer.

theorem HCPolySupport.hasHodgeConverse_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) : HasHodgeConverse U

Packaged version of hodgeConverseCriterion_of_isOpenBoundedConvexDomain.

theorem HCPolySupport.IsPotentialOn.potential_of_orthogonalL2 {d : ℕ} {U : Set (Vec d)} (h : HodgeConverseCriterion U) {f : Vec d → Vec d} (hf : MemVectorL2 U f) (horth : ∀ {g : Vec d → Vec d}, MemVectorL2 U g → IsSolenoidalZeroNormalTraceOn U g → ∫ (x : Vec d) in U, vecDot (g x) (f x) = 0) : IsPotentialOn U f

theorem HCPolySupport.IsPotentialOn.of_orthogonal_to_solenoidalZeroNormalTrace_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] [HasHodgeConverse U] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (horth : ∀ {g : Vec d → Vec d}, MemVectorL2 U g → IsSolenoidalZeroNormalTraceOn U g → ∫ (x : Vec d) in U, vecDot (g x) (f x) = 0) : IsPotentialOn U f

theorem HCPolySupport.IsPotentialOn.of_orthogonal_to_solenoidalZeroNormalTrace_of_memVectorL2_of_h1CoerciveEstimate {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) {f : Vec d → Vec d} (hf : MemVectorL2 U f) (horth : ∀ {g : Vec d → Vec d}, MemVectorL2 U g → IsSolenoidalZeroNormalTraceOn U g → ∫ (x : Vec d) in U, vecDot (g x) (f x) = 0) : IsPotentialOn U f

theorem HCPolySupport.IsPotentialOn.restrict_of_isOpen_of_memVectorL2 {d : ℕ} {U V : Set (Vec d)} {f : Vec d → Vec d} (hf : IsPotentialOn U f) (_hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hfV : MemVectorL2 V f) : IsPotentialOn V f