The completed resisting objective's gradient remains large outside the central region.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpNorm_supporting_vector_dual_norm_eq_one {d : ℕ} {p : ℝ} (hp : 1 < p) {y g : Point d} (hy : y ≠ 0) (hsupport : ∀ (z : Point d), lpNorm p y + O3.pairing g (z - y) ≤ lpNorm p z) : lpNorm (conjugateExponent p) g = 1

Every supporting vector of the nonzero ell_p norm has exact dual norm one. The upper estimate uses the repository's kernel-closed norming vector.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.kernel_radial_barrier_of_unit_boundary {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (hp : 1 ≤ p) (hconv : O3.IsConvexObjective kernel.phi) (hphi0 : kernel.phi 0 = 0) (hboundary : ∀ (u : Point d), lpNorm p u = 1 → kernel.phi u > lpNorm p u) (u : Point d) : 1 ≤ lpNorm p u → lpNorm p u < kernel.phi u

Convexity and the frozen strict unit-sphere boundary condition propagate to the all-radii barrier required by compact-ball attainment.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.supporting_vector_eq_coordinate_gradient {d : ℕ} (f : Point d → ℝ) (gradient : Point d → Point d) (x g : Point d) (hgradient : O3.IsCoordinateGradient f gradient) (hsupport : ∀ (z : O3.Point d), f x + O3.pairing g (z - x) ≤ f z) : g = gradient x

A global supporting vector of a genuinely differentiable value is its actual coordinate gradient. This is Fermat's theorem applied after removing the supporting affine functional.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.shiftedLpNorm_convex_oneLipschitz {d : ℕ} {p c : ℝ} (hp : 1 ≤ p) : (O3.IsConvexObjective fun (x : Point d) => lpNorm p x - c) ∧ IsOneLipschitz p fun (x : Point d) => lpNorm p x - c

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialG_le_lpNorm {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {t : ℕ} (hp : 1 ≤ p) (hdelta : 0 ≤ data.delta) (hxi : ∀ i ≤ t, data.xi i = 1 ∨ data.xi i = -1) (hres : ResistingMaximumAt data t) (x : Point d) : data.partialG t x ≤ lpNorm p x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialH_eq_shiftedLpNorm_of_three_le {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {t : ℕ} (hp : 1 ≤ p) (hdelta : 0 ≤ data.delta) (hxi : ∀ i ≤ t, data.xi i = 1 ∨ data.xi i = -1) (hres : ResistingMaximumAt data t) (hH : ∀ (x : Point d), data.partialH t x = max (data.partialG t x / 2) (lpNorm p x - 3 / 2)) {x : Point d} (hx : 3 ≤ lpNorm p x) : data.partialH t x = lpNorm p x - 3 / 2

theorem V7.Stage5AboveTwoLowerS5A2Envelope.smooth_shiftedLpNorm_gradient_dual_norm_eq_one {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (hp : 1 < p) {chi : ℝ} (hchi : 0 < chi) (hkernel : SmoothingKernelAssumptions kernel) {x : Point d} (hx : chi < lpNorm p x) : lpNorm (conjugateExponent p) ((kernel.smooth chi fun (z : Point d) => lpNorm p z - 3 / 2).gradient x) = 1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.coordinateGradient_eq_zero_of_global_minimizer {d : ℕ} (f : Point d → ℝ) (gradient : Point d → Point d) (x : Point d) (hgradient : O3.IsCoordinateGradient f gradient) (hmin : ∀ (y : Point d), f x ≤ f y) : gradient x = 0

theorem V7.aboveLowerOutsideGradient : AboveLowerOutsideGradientStatement

Frozen S5-D outside-gradient and optimizer-interiority package.