Stage 10: Euclidean guard semantics

Every observable source guard is proved to pass when the trial scale dominates the true smoothness constant. In particular, the ordered interpolation inequality is derived from convexity and the exact L/2 descent lemma; it is not assumed as a certificate.

theorem O3.euclidean_interpolation_of_smooth_convex {d : ℕ} (P : AdmissibleInstance d 2) (x y : Vec d) : lpNorm 2 (P.grad x - P.grad y) ^ 2 / (2 * P.L) ≤ P.f x - P.f y - pairing (P.grad y) (x - y)

The exact Euclidean smooth-convex interpolation inequality.

theorem O3.euclideanInterpolationGuard_holds_of_le {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (hM : 0 < M) (hLM : P.L ≤ M) (x y : Vec d) : (interpolationGuard (P.f x) (P.f y) (pairing (P.grad y) (x - y)) (lpNorm 2 (P.grad x - P.grad y) ^ 2) M).Holds

If L ≤ M, every ordered finite-data interpolation guard passes.

theorem O3.euclideanEstimateGuard_holds_of_le {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (hLM : P.L ≤ M) (k : ℕ) : (euclideanEstimateGuard P M k).Holds

Every actual Phase-A upper-model guard passes under L ≤ M.

theorem O3.ogmgTerminalDescentCheck_holds_of_le {d : ℕ} (P : AdmissibleInstance d 2) (cfg : OGMGExecutionConfig d) (hcfg : cfg.oracle = P.oracle) {M : ℝ} (hcfgM : cfg.M = M) (hLM : P.L ≤ M) : (ogmgTerminalDescentCheck cfg).Holds

The actual Stage-9 terminal descent guard passes under L ≤ M.