The completed resisting oracle preserves all earlier exact value-gradient observations.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialG_convex {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {t : ℕ} (ht : t < T) (hsteps : ∀ s < T, (data.xi s = 1 ∨ data.xi s = -1) ∧ ResistingMaximumAt data s) : O3.IsConvexObjective (data.partialG t)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialG_oneLipschitz {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {t : ℕ} (hp : 1 ≤ p) (ht : t < T) (hsteps : ∀ s < T, (data.xi s = 1 ∨ data.xi s = -1) ∧ ResistingMaximumAt data s) : IsOneLipschitz p (data.partialG t)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialH_convex_oneLipschitz {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {t : ℕ} (hp : 1 ≤ p) (ht : t < T) (hsteps : ∀ s < T, (data.xi s = 1 ∨ data.xi s = -1) ∧ ResistingMaximumAt data s) (hH : ∀ (x : Point d), data.partialH t x = max (data.partialG t x / 2) (lpNorm p x - 3 / 2)) : O3.IsConvexObjective (data.partialH t) ∧ IsOneLipschitz p (data.partialH t)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.future_piece_le_at_nearby_query {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 1 ≤ p) (hdelta : 0 < data.delta) (hchi : data.delta = 2 * data.chi) (hsteps : ∀ s < T, (∀ r < s, data.sigma r ≠ data.sigma s) ∧ ↑(data.sigma s) < T ∧ (∀ (j : Fin d), ↑j < T → (∀ r < s, data.sigma r ≠ j) → |data.queries s j| ≤ |data.queries s (data.sigma s)|) ∧ (data.xi s = 1 ∨ data.xi s = -1) ∧ data.xi s * data.queries s (data.sigma s) = |data.queries s (data.sigma s)| ∧ ResistingMaximumAt data s ∧ (∀ (x : Point d), data.partialH s x = max (data.partialG s x / 2) (lpNorm p x - 3 / 2)) ∧ (∀ (x : O3.Vec d), (data.partialOracle s).value x = data.beta * (data.kernel.smooth data.chi (data.partialH s)).value x) ∧ ∀ (x : O3.Vec d), (data.partialOracle s).gradient x = data.beta • (data.kernel.smooth data.chi (data.partialH s)).gradient x) {t i : ℕ} (ht : t < T) (hi : i < T) (hti : t < i) (v : Point d) (hv : lpNorm p v ≤ data.chi) : data.xi i * (data.queries t + v) (data.sigma i) - ↑i * data.delta ≤ data.xi t * (data.queries t + v) (data.sigma t) - ↑t * data.delta

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialG_final_eq_at_nearby_query {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 1 ≤ p) (hT : 1 ≤ T) (hdelta : 0 < data.delta) (hchi : data.delta = 2 * data.chi) (hsteps : ∀ s < T, (∀ r < s, data.sigma r ≠ data.sigma s) ∧ ↑(data.sigma s) < T ∧ (∀ (j : Fin d), ↑j < T → (∀ r < s, data.sigma r ≠ j) → |data.queries s j| ≤ |data.queries s (data.sigma s)|) ∧ (data.xi s = 1 ∨ data.xi s = -1) ∧ data.xi s * data.queries s (data.sigma s) = |data.queries s (data.sigma s)| ∧ ResistingMaximumAt data s ∧ (∀ (x : Point d), data.partialH s x = max (data.partialG s x / 2) (lpNorm p x - 3 / 2)) ∧ (∀ (x : O3.Vec d), (data.partialOracle s).value x = data.beta * (data.kernel.smooth data.chi (data.partialH s)).value x) ∧ ∀ (x : O3.Vec d), (data.partialOracle s).gradient x = data.beta • (data.kernel.smooth data.chi (data.partialH s)).gradient x) {t : ℕ} (ht : t < T) (v : Point d) (hv : lpNorm p v ≤ data.chi) : data.partialG (T - 1) (data.queries t + v) = data.partialG t (data.queries t + v)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialH_final_eq_at_nearby_query {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 1 ≤ p) (hT : 1 ≤ T) (hdelta : 0 < data.delta) (hchi : data.delta = 2 * data.chi) (hsteps : ∀ s < T, (∀ r < s, data.sigma r ≠ data.sigma s) ∧ ↑(data.sigma s) < T ∧ (∀ (j : Fin d), ↑j < T → (∀ r < s, data.sigma r ≠ j) → |data.queries s j| ≤ |data.queries s (data.sigma s)|) ∧ (data.xi s = 1 ∨ data.xi s = -1) ∧ data.xi s * data.queries s (data.sigma s) = |data.queries s (data.sigma s)| ∧ ResistingMaximumAt data s ∧ (∀ (x : Point d), data.partialH s x = max (data.partialG s x / 2) (lpNorm p x - 3 / 2)) ∧ (∀ (x : O3.Vec d), (data.partialOracle s).value x = data.beta * (data.kernel.smooth data.chi (data.partialH s)).value x) ∧ ∀ (x : O3.Vec d), (data.partialOracle s).gradient x = data.beta • (data.kernel.smooth data.chi (data.partialH s)).gradient x) {t : ℕ} (ht : t < T) (v : Point d) (hv : lpNorm p v ≤ data.chi) : data.partialH (T - 1) (data.queries t + v) = data.partialH t (data.queries t + v)

theorem V7.aboveLowerExactPairCompletion : AboveLowerExactPairCompletionStatement

Frozen S5-B: the completed oracle returns exactly the same value-gradient pair as the chronological partial oracle at every counted query.