← Mathematical handbook

Contact rigidity of a Lipschitz dual potential

theorem Verification.dual_potential_negative (g : ℝ → ℝ) (v : NNReal) (θ : ℝ) (hg : LipschitzWith v g) (hθ : ↑v < θ) (hf : ∀ (a b : ℝ), g a + g b ≤ (b - a) ^ 2 - θ * |b - a|) (a : ℝ) : g a < 0

A globally feasible dual potential is strictly negative when its Lipschitz constant is smaller than the distance coefficient. This excludes diagonal contact.

theorem Verification.dual_upper_contact (g : ℝ → ℝ) (θ a b : ℝ) (hf : ∀ (x y : ℝ), g x + g y ≤ (y - x) ^ 2 - θ * |y - x|) (hab : a < b) (hd : DifferentiableAt ℝ g a) (he : g a + g b = (b - a) ^ 2 - θ * |b - a|) : b = a + (θ - deriv g a) / 2

At a differentiability point, the dual contact above the diagonal has one possible endpoint. No explicit case split over the spline pieces is needed.