Convexity, coordinate gradients, and lower bounds survive affine oracle normalization.

theorem V7.Stage3BelowTwoS3F.normalized_coordinateGradient {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (c : Point d) {M D : ℝ} (hM : 0 < M) (hD : 0 < D) : O3.IsCoordinateGradient (normalizedPairOracle c M D inst.oracle).value (normalizedPairOracle c M D inst.oracle).gradient

theorem V7.Stage3BelowTwoS3F.normalized_convex {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (c : Point d) {M D : ℝ} (hM : 0 < M) (hD : 0 < D) : O3.IsConvexObjective (normalizedPairOracle c M D inst.oracle).value

theorem V7.Stage3BelowTwoS3F.normalized_bddBelow {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) (c : Point d) {M D : ℝ} (hM : 0 < M) : BddBelow (Set.range (normalizedPairOracle c M D inst.oracle).value)