Physical rescaling preserves convexity, gradients, smoothness, and the prescribed minimizer distance.

theorem V7.Stage5AboveTwoLowerS5F.physicalOracle_coordinateGradient {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hL : 0 < L) (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (hgrad : O3.IsCoordinateGradient bar.value bar.gradient) : O3.IsCoordinateGradient (physicalOracle x0 L R rT bar).value (physicalOracle x0 L R rT bar).gradient

theorem V7.Stage5AboveTwoLowerS5F.physicalOracle_convex {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hL : 0 < L) (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (hconv : O3.IsConvexObjective bar.value) : O3.IsConvexObjective (physicalOracle x0 L R rT bar).value

theorem V7.Stage5AboveTwoLowerS5F.physicalBackward_sub {d : ℕ} (x0 : Point d) (R rT : ℝ) (x y : Point d) : physicalBackward x0 R rT x - physicalBackward x0 R rT y = (rT / R) • (x - y)

theorem V7.Stage5AboveTwoLowerS5F.physicalOracle_smooth {p : ℝ} {d : ℕ} (hp : 2 < p) (x0 : Point d) {L R rT : ℝ} (hL : 0 < L) (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (hsmooth : IsLpSmooth p 1 bar) : IsLpSmooth p L (physicalOracle x0 L R rT bar)

theorem V7.Stage5AboveTwoLowerS5F.physical_minimizer_iff {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hL : 0 < L) (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (x : Point d) : x ∈ O3.MinimizerSet (physicalOracle x0 L R rT bar).value ↔ physicalBackward x0 R rT x ∈ O3.MinimizerSet bar.value

theorem V7.Stage5AboveTwoLowerS5F.physical_minimizerNonempty {d : ℕ} (x0 : Point d) {L R rT : ℝ} (hL : 0 < L) (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (hne : (O3.MinimizerSet bar.value).Nonempty) : (O3.MinimizerSet (physicalOracle x0 L R rT bar).value).Nonempty

theorem V7.Stage5AboveTwoLowerS5F.physical_minimizerDistance {d : ℕ} {p : ℝ} (hp : 2 < p) (x0 : Point d) {L R rT : ℝ} (hL : 0 < L) (hR : 0 < R) (hrT : 0 < rT) (bar : PairOracle d) (hradius : minimizerDistance p bar 0 = rT) : minimizerDistance p (physicalOracle x0 L R rT bar) x0 = R