SuperposedDivergencePotential

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

Solenoidality of the superposed divergence from potential basis defects

This file connects the geometric G field already defined in SuperposedDivergence.lean to the model-free antisymmetric-divergence theorem of H10SkewDivergence.lean.

The only analytic input is the internally produced hFbasis interface: each basis-load slope defect is a public zero-trace potential field. Choosing its H¹₀ witness identifies the superposed divergence defect almost everywhere with h10SkewMatrixDiv; no continuity, local-finiteness, mesh, or trace hypothesis is added here.

Pointwise algebra

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorDivergence_sub_eq {d : ℕ} (hd : 2 ≤ d) (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (q x : HCPolySupport.Vec d) : superposedCompetitorDivergence m hn I q x - q = fun (j : Fin d) => (↑d - 1)⁻¹ * ((∑ i : Fin d, (superposedCompetitorSlope m hn I (HCPolySupport.basisVec i) x - HCPolySupport.basisVec i) i) * q j - ∑ i : Fin d, q i * (superposedCompetitorSlope m hn I (HCPolySupport.basisVec j) x - HCPolySupport.basisVec j) i)

Pointwise deviation identity for the superposed divergence field. With u_i = ∇ℓ̂_{e_i} - e_i, it reads

∇·D̂_q - q = (d-1)⁻¹ ((∑_i (u_i)_i) q - u_·ᵀ q).

Conditional local G-leg A

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorDivergence_sub_solenoidalZeroNormalTraceFieldOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hd : 2 ≤ d) (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (q : HCPolySupport.Vec d) (hFbasis : ∀ (i : Fin d), HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U fun (x : HCPolySupport.Vec d) => superposedCompetitorSlope m hn I (HCPolySupport.basisVec i) x - HCPolySupport.basisVec i) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U fun (x : HCPolySupport.Vec d) => superposedCompetitorDivergence m hn I q x - q

If every basis-load superposed slope defect is a public zero-trace potential field on U, then the superposed divergence defect is a public solenoidal field with zero normal trace on U.

The hFbasis premise is an internal producer interface. It is the exact finite family needed to construct the antisymmetric matrix; it is not an additional hypothesis of any frozen theorem.

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorDivergence_sub_solenoidalZeroNormalTraceFieldOn_of_forall {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hd : 2 ≤ d) (m : ℤ) (hn : ℕ → ℕ) (I : Set (HCPolySupport.TriadicCube d)) (q : HCPolySupport.Vec d) (hF : ∀ (p : HCPolySupport.Vec d), HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U fun (x : HCPolySupport.Vec d) => superposedCompetitorSlope m hn I p x - p) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U fun (x : HCPolySupport.Vec d) => superposedCompetitorDivergence m hn I q x - q

Arbitrary-load form of the conditional bridge. It specializes the potential hypothesis only at the basis vectors used by D̂_q.