The physical above-two phase observations, guard schedules, and terminal outcome shapes.

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseOneOracle {d : ℕ} (x0 : Point d) (M D : ℝ) (oracle : PairOracle d) : PairOracle d

The above-two primal oracle normalized around the initial point.

Equations

• V7.Stage4AboveTwoFinalTrial.phaseOneOracle x0 M D oracle = V7.normalizedPairOracle x0 M D oracle

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseOneState {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : PrimalState d

The normalized primal state at the prescribed primal budget and horizon.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseOneObs {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : Observation d

The physical oracle observation at a normalized above-two primal iterate.

Equations

• V7.Stage4AboveTwoFinalTrial.phaseOneObs p eps M D x0 oracle k = O3.PairOracle.observe oracle (x0 + D • (V7.Stage4AboveTwoFinalTrial.phaseOneState p eps M D x0 oracle k).x)

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseTwoCenter {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) : Point d

The completed primal endpoint used as the physical center of the dual phase.

Equations

• V7.Stage4AboveTwoFinalTrial.phaseTwoCenter p eps M D x0 oracle = (V7.Stage4AboveTwoFinalTrial.phaseOneObs p eps M D x0 oracle (V7.Stage4AboveTwoFinalTrial.nF p eps M D)).point

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseTwoOracle {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) : PairOracle d

The above-two dual oracle normalized around the primal endpoint.

Equations

• V7.Stage4AboveTwoFinalTrial.phaseTwoOracle p eps M D x0 oracle = V7.normalizedPairOracle (V7.Stage4AboveTwoFinalTrial.phaseTwoCenter p eps M D x0 oracle) M D oracle

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseTwoObs {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) : Observation d

The physical oracle observation at a normalized above-two dual query.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseOneNewTrace {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : List (Observation d)

The new primal observations after the reused initial query.

Equations

• V7.Stage4AboveTwoFinalTrial.phaseOneNewTrace p eps M D x0 oracle m = List.map (fun (k : ℕ) => V7.Stage4AboveTwoFinalTrial.phaseOneObs p eps M D x0 oracle (k + 1)) (List.range m)

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseTwoNewTrace {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : List (Observation d)

The new dual observations after the reused primal endpoint.

Equations

• V7.Stage4AboveTwoFinalTrial.phaseTwoNewTrace p eps M D x0 oracle m = List.map (fun (k : ℕ) => V7.Stage4AboveTwoFinalTrial.phaseTwoObs p eps M D x0 oracle (k + 1)) (List.range m)

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseOneChecks {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : List (ObservableGuardCheck d)

The consecutive cocoercivity checks in the completed above-two primal prefix.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage4AboveTwoFinalTrial.phaseTwoChecks {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) : List (ObservableGuardCheck d)

The consecutive cocoercivity checks in the completed above-two dual prefix.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage4AboveTwoFinalTrial.allChecks {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m₁ m₂ : ℕ) : List (ObservableGuardCheck d)

The ordered guard checks from the completed prefixes of both above-two phases.

Equations

• One or more equations did not get rendered due to their size.

inductive V7.Stage4AboveTwoFinalTrial.FullShape {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) : TrialReport d → ℕ → ℕ → Prop

The possible success, scale-failure, and radius outcomes of an above-two trial report.

• primalSuccess {d : ℕ} {p eps M D : ℝ} {x0 : Point d} {oracle : PairOracle d} (m : ℕ) (hm0 : 0 < m) (hmn : m ≤ nF p eps M D) (hsmall : lpNorm (conjugateExponent p) (phaseOneObs p eps M D x0 oracle m).gradient ≤ eps) (hprior : ∀ k < m - 1, Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))) : FullShape p eps M D x0 oracle { trace := phaseOneNewTrace p eps M D x0 oracle m, checkedGuards := phaseOneChecks p eps M D x0 oracle (m - 1), outcome := TrialOutcome.success (phaseOneObs p eps M D x0 oracle m) } m 0
• primalScale {d : ℕ} {p eps M D : ℝ} {x0 : Point d} {oracle : PairOracle d} (m : ℕ) (hm0 : 0 < m) (hmn : m ≤ nF p eps M D) (hprior : ∀ k < m - 1, Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))) (hlarge : eps < lpNorm (conjugateExponent p) (phaseOneObs p eps M D x0 oracle m).gradient) (hfail : ¬Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle (m - 1)) (phaseOneObs p eps M D x0 oracle m)) : FullShape p eps M D x0 oracle { trace := phaseOneNewTrace p eps M D x0 oracle m, checkedGuards := phaseOneChecks p eps M D x0 oracle m, outcome := TrialOutcome.scale (Stage3BelowTwoS3F.cocoCheck (phaseOneObs p eps M D x0 oracle (m - 1)) (phaseOneObs p eps M D x0 oracle m)) } m 0
• dualSuccess {d : ℕ} {p eps M D : ℝ} {x0 : Point d} {oracle : PairOracle d} (m : ℕ) (hm0 : 0 < m) (hmn : m ≤ nD p eps M D) (hP : ∀ k < nF p eps M D, Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))) (hQ : ∀ k < m - 1, Stage3BelowTwoS3F.cocoPairHolds p M (phaseTwoObs p eps M D x0 oracle k) (phaseTwoObs p eps M D x0 oracle (k + 1))) (hsmall : lpNorm (conjugateExponent p) (phaseTwoObs p eps M D x0 oracle m).gradient ≤ eps) : FullShape p eps M D x0 oracle { trace := phaseOneNewTrace p eps M D x0 oracle (nF p eps M D) ++ phaseTwoNewTrace p eps M D x0 oracle m, checkedGuards := allChecks p eps M D x0 oracle (nF p eps M D) (m - 1), outcome := TrialOutcome.success (phaseTwoObs p eps M D x0 oracle m) } (nF p eps M D) m
• dualScale {d : ℕ} {p eps M D : ℝ} {x0 : Point d} {oracle : PairOracle d} (m : ℕ) (hm0 : 0 < m) (hmn : m ≤ nD p eps M D) (hP : ∀ k < nF p eps M D, Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))) (hQ : ∀ k < m - 1, Stage3BelowTwoS3F.cocoPairHolds p M (phaseTwoObs p eps M D x0 oracle k) (phaseTwoObs p eps M D x0 oracle (k + 1))) (hlarge : eps < lpNorm (conjugateExponent p) (phaseTwoObs p eps M D x0 oracle m).gradient) (hfail : ¬Stage3BelowTwoS3F.cocoPairHolds p M (phaseTwoObs p eps M D x0 oracle (m - 1)) (phaseTwoObs p eps M D x0 oracle m)) : FullShape p eps M D x0 oracle { trace := phaseOneNewTrace p eps M D x0 oracle (nF p eps M D) ++ phaseTwoNewTrace p eps M D x0 oracle m, checkedGuards := allChecks p eps M D x0 oracle (nF p eps M D) m, outcome := TrialOutcome.scale (Stage3BelowTwoS3F.cocoCheck (phaseTwoObs p eps M D x0 oracle (m - 1)) (phaseTwoObs p eps M D x0 oracle m)) } (nF p eps M D) m
• radius {d : ℕ} {p eps M D : ℝ} {x0 : Point d} {oracle : PairOracle d} (hP : ∀ k < nF p eps M D, Stage3BelowTwoS3F.cocoPairHolds p M (phaseOneObs p eps M D x0 oracle k) (phaseOneObs p eps M D x0 oracle (k + 1))) (hQ : ∀ k < nD p eps M D, Stage3BelowTwoS3F.cocoPairHolds p M (phaseTwoObs p eps M D x0 oracle k) (phaseTwoObs p eps M D x0 oracle (k + 1))) (hlarge : eps < lpNorm (conjugateExponent p) (phaseTwoObs p eps M D x0 oracle (nD p eps M D)).gradient) : FullShape p eps M D x0 oracle { trace := phaseOneNewTrace p eps M D x0 oracle (nF p eps M D) ++ phaseTwoNewTrace p eps M D x0 oracle (nD p eps M D), checkedGuards := allChecks p eps M D x0 oracle (nF p eps M D) (nD p eps M D), outcome := TrialOutcome.radius (phaseTwoObs p eps M D x0 oracle (nD p eps M D)) } (nF p eps M D) (nD p eps M D)