Neighborhood equality of smooth objective values determines the complete exact oracle pair.

theorem V7.Stage5AboveTwoLower.observe_eq_of_eventually_value_eq {d : ℕ} (oracle₁ oracle₂ : PairOracle d) (x : Point d) (hgrad₁ : O3.IsCoordinateGradient oracle₁.value oracle₁.gradient) (hgrad₂ : O3.IsCoordinateGradient oracle₂.value oracle₂.gradient) (hlocal : oracle₁.value =ᶠ[nhds x] oracle₂.value) : O3.PairOracle.observe oracle₁ x = O3.PairOracle.observe oracle₂ x

Once two differentiable smoothing values agree on a neighbourhood, their exact value-gradient observations agree at the centre. Thus the analytic content of exact-pair locality is precisely neighbourhood stability of the infimal convolution, not a separate gradient oracle assumption.

def V7.Stage5AboveTwoLower.LocalSmoothingNeighborhoodStability {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) : Prop

The minimal analytic bridge still needed from the concrete infimal convolution: equality of the original objectives on the closed smoothing ball must make the two smoothed value functions equal on a neighbourhood of the centre. The strict boundary inequality of the kernel is what supplies the required interior slack.

Equations

• One or more equations did not get rendered due to their size.

def V7.Stage5AboveTwoLower.SmoothingCoordinateGradientCore {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) : Prop

Smoothing a convex one-Lipschitz objective produces an oracle with the exact coordinate gradient.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage5AboveTwoLower.exact_pair_locality_of_neighborhood_stability {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (hgradient : SmoothingCoordinateGradientCore kernel) (hstable : LocalSmoothingNeighborhoodStability kernel) (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 (kernel.smooth chi ell₁) x = O3.PairOracle.observe (kernel.smooth chi ell₂) x

Neighbourhood stability plus the already required coordinate-gradient interface is sufficient for the frozen exact value-gradient locality clause.