PotentialComparison

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

Weak comparison with a bounded nonnegative potential

The general potential comparison is provided by PotentialOrder; WeakSubsolution derives its zero-potential specialization. This public import path is retained for callers.