Minimizing displacements give global supporting inequalities for the smoothing envelope.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.localSmoothingValue_supporting_of_minimizers {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (hconv : O3.IsConvexObjective ell) (hconvPhi : O3.IsConvexObjective kernel.phi) (hgradPhi : O3.IsCoordinateGradient kernel.phi kernel.gradPhi) {x z v w : Point d} (hv : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v) (hw : Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell z w) : localSmoothingValue kernel chi ell x + O3.pairing (-kernel.gradPhi ((1 / chi) • v)) (z - x) ≤ localSmoothingValue kernel chi ell z

A minimizer supplies a genuine global supporting vector for the literal infimal value. The proof combines the locally built nonsmooth optimality relation with first-order convexity of the smooth kernel.