ShellLawJ4

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

structure Algsuperdiff.Frozen.Assumptions.ShellLawJ4 (d : ℕ) (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (_dimension : 2 ≤ d) (hJ1 : ShellLawJ1 d P) (hJ2 : ShellLawJ2 d P) : Prop

ABK26 (J4): one positive non-degeneracy constant, shared by every unit vector, gives the exact stationary potential-corrector energy. The stationarity and L² proofs consumed by the canonical corrector are derived from (J1) and (J2), not added as J4 hypotheses.

• nondegenerate : ∃ (cstar : ℝ), 0 < cstar ∧ ∀ (e : { e : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm e = 1 }), ‖ShellField.zeroShellPotentialCorrector P ⋯ ↑e ⋯‖ ^ 2 = cstar * Real.log 3