The selected envelope gradient closes the smoothing kernel's derivative, smoothness, and locality properties.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_localValue_eq_base (p : ℝ) (d : ℕ) (chi : ℝ) (ell : Point d → ℝ) (x : Point d) : localSmoothingValue (repairKernel p d) chi ell x = localSmoothingValue (repairKernelBase p d) chi ell x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_value_realization {p : ℝ} {d : ℕ} (chi : ℝ) : 0 < chi → ∀ (ell : Point d → ℝ), O3.IsConvexObjective ell → IsOneLipschitz p ell → ∀ (x : O3.Vec d), ((repairKernel p d).smooth chi ell).value x = localSmoothingValue (repairKernel p d) chi ell x

The constructed oracle value is the literal frozen infimal convolution.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_coordinateGradient {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : Stage5AboveTwoLower.SmoothingCoordinateGradientCore (repairKernel p d)

Genuine ambient coordinate derivative for the literal infimal value.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_smooth {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (chi : ℝ) : 0 < chi → ∀ (ell : Point d → ℝ), O3.IsConvexObjective ell → IsOneLipschitz p ell → IsLpSmooth p ((repairKernel p d).Mpd / chi) ((repairKernel p d).smooth chi ell)

Exact frozen Mpd/chi smoothness, with no ambient conversion in the final estimate.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_exactPairLocality {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (chi : ℝ) : 0 < chi → ∀ (ell₁ ell₂ : Point d → ℝ), O3.IsConvexObjective ell₁ → IsOneLipschitz p ell₁ → O3.IsConvexObjective ell₂ → IsOneLipschitz p ell₂ → ∀ (x : O3.Vec d), (∀ (v : Point d), lpNorm p v ≤ chi → ell₁ (x + v) = ell₂ (x + v)) → O3.PairOracle.observe ((repairKernel p d).smooth chi ell₁) x = O3.PairOracle.observe ((repairKernel p d).smooth chi ell₂) x

The value-level locality already closed in the prefix upgrades to exact value-gradient observations for the genuine derivative oracle.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.s5a2_envelope_derivative_smoothness_closed {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : (∀ (chi : ℝ), 0 < chi → ∀ (ell : Point d → ℝ), O3.IsConvexObjective ell → IsOneLipschitz p ell → ∀ (x : O3.Vec d), ((repairKernel p d).smooth chi ell).value x = localSmoothingValue (repairKernel p d) chi ell x) ∧ Stage5AboveTwoLower.SmoothingCoordinateGradientCore (repairKernel p d) ∧ (∀ (chi : ℝ), 0 < chi → ∀ (ell : Point d → ℝ), O3.IsConvexObjective ell → IsOneLipschitz p ell → IsLpSmooth p ((repairKernel p d).Mpd / chi) ((repairKernel p d).smooth chi ell)) ∧ ∀ (chi : ℝ), 0 < chi → ∀ (ell₁ ell₂ : Point d → ℝ), O3.IsConvexObjective ell₁ → IsOneLipschitz p ell₁ → O3.IsConvexObjective ell₂ → IsOneLipschitz p ell₂ → ∀ (x : O3.Vec d), (∀ (v : Point d), lpNorm p v ≤ chi → ell₁ (x + v) = ell₂ (x + v)) → O3.PairOracle.observe ((repairKernel p d).smooth chi ell₁) x = O3.PairOracle.observe ((repairKernel p d).smooth chi ell₂) x

S5-A2 closure package, separated from the remaining signed-equivariance clauses of the full S5-A carrier.