The Euclidean source execution connected to the analytic gap and terminal-gradient estimates.

theorem V7.Stage1E03.positive_fstar_eq_minimizer {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) {xstar : Point d} (hxstar : xstar ∈ MinimizerSet inst.oracle) : inst.fstar = inst.oracle.value xstar

theorem V7.Stage1E03.positive_fstar_eq_sInf_range {p : ℝ} {d : ℕ} {x0 : Point d} (inst : PositiveInstance p d x0) : inst.fstar = sInf (Set.range inst.oracle.value)

theorem V7.Stage1E03.source_current_analytic_bridge {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M D : ℝ) (n : ℕ) (hM : 0 < M) (hn : 1 ≤ n) (hDR : inst.R ≤ D) (report : TrialReport d) (hall : ∀ check ∈ report.checkedGuards, CheckHolds 2 M check) (hguards : report.checkedGuards = sourceGuardSchedule inst M n) : have phaseA := sourcePhaseAData inst M D n; have phaseB := sourcePhaseBData inst M n (sourceU inst M n); (phaseA.inst.oracle.value (phaseA.x n) - phaseA.inst.fstar ≤ phaseA.M * phaseA.D ^ 2 / (2 * phaseA.A n) ∧ phaseA.M * phaseA.D ^ 2 / (2 * phaseA.A n) ≤ 2 * phaseA.M * phaseA.D ^ 2 / (↑n + 1) ^ 2) ∧ lpNorm 2 (phaseB.oracle.gradient (phaseB.u n)) ^ 2 ≤ 2 * phaseB.M * (phaseB.oracle.value phaseB.U - phaseB.fstar) / phaseB.theta 0 ^ 2 ∧ phaseB.theta 0 ≥ (↑n + 1) / √2

theorem V7.Stage1E03.source_current_gradient_bound {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M D : ℝ) (n : ℕ) (hM : 0 < M) (hD : 0 < D) (hn : 1 ≤ n) (hDR : inst.R ≤ D) (report : TrialReport d) (hall : ∀ check ∈ report.checkedGuards, CheckHolds 2 M check) (hguards : report.checkedGuards = sourceGuardSchedule inst M n) : lpNorm 2 (inst.oracle.gradient ((sourcePhaseBData inst M n (sourceU inst M n)).u n)) ≤ 2 * √2 * M * D / ((↑n + 1) * (↑n + 1))

The scalar consequence needed by the radius branch, derived from the current frozen E01/E02 carriers rather than from the legacy Stage-10 composition theorem.