The explicit above-two trial supplied to the known-parameter upper-bound argument.

theorem V7.Stage5AboveTwoLowerS5F.explicit_aboveLocalTrial {d : ℕ} (p : ℝ) (hp : 2 < p) (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) (inst : PositiveInstance p d x0) (hcached : cached.observation = O3.PairOracle.observe inst.oracle x0) (hG : eps < lpNorm (conjugateExponent p) (inst.oracle.gradient x0)) (hDG : D ≥ lpNorm (conjugateExponent p) (inst.oracle.gradient x0) / M) : have nf := Stage4AboveTwoFinalTrial.nF p eps M D; have nd := Stage4AboveTwoFinalTrial.nD p eps M D; ∃ (report : TrialReport d) (w : AboveTrialWitness p d), (Stage4AboveTwoFinalTrial.aboveLocalTrial p eps x0 nf nd).Executes M D cached inst.oracle report ∧ TrialCertificate eps p M D inst.L inst.R cached inst.oracle report ∧ AboveTrialOperationalContract p eps M D x0 cached inst.oracle report w ∧ ↑report.calls ≤ Stage4AboveTwoFinalTrial.trialConstant p * (M * D / eps) ^ (p / (p + 2))