Compatibility and soundness of the current observable guards and the original analytic inequalities.

theorem V7.upperModelGuard_of_scale_ge {d : ℕ} {x0 : Point d} {p L M : ℝ} (hp : 1 < p) (inst : PositiveInstance p d x0) (hLM : L ≤ M) (hL : inst.L = L) (x y : Point d) : UpperModelGuard p M inst.oracle x y

theorem V7.failed_upperModelGuard_lt_trueScale {d : ℕ} {x0 : Point d} {p L M : ℝ} (hp : 1 < p) (inst : PositiveInstance p d x0) (hL : inst.L = L) (x y : Point d) (hfail : ¬UpperModelGuard p M inst.oracle x y) : M < L

theorem V7.gradientGuard_of_scale_ge {d : ℕ} {x0 : Point d} {p L M : ℝ} (inst : PositiveInstance p d x0) (hLM : L ≤ M) (hL : inst.L = L) (x y : Point d) : GradientGuard p M inst.oracle x y

theorem V7.failed_gradientGuard_lt_trueScale {d : ℕ} {x0 : Point d} {p L M : ℝ} (inst : PositiveInstance p d x0) (hL : inst.L = L) (x y : Point d) (hfail : ¬GradientGuard p M inst.oracle x y) : M < L

theorem V7.upperModelGuard_iff_historical {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (x y : Point d) : UpperModelGuard p M oracle x y ↔ (O3.upperModelGuard (oracle.value x) (oracle.value y) (pairing (oracle.gradient x) (y - x)) (lpNorm p (y - x) ^ 2) M).Holds

theorem V7.euclideanInterpolationGuard_iff_historical {d : ℕ} (M : ℝ) (oracle : PairOracle d) (x y : Point d) : EuclideanInterpolationGuard M oracle x y ↔ (O3.interpolationGuard (oracle.value x) (oracle.value y) (pairing (oracle.gradient y) (x - y)) (lpNorm 2 (oracle.gradient x - oracle.gradient y) ^ 2) M).Holds