The below-two trial's query count is bounded by its accuracy-dependent horizon.

theorem V7.Stage3BelowTwoS3F.calls_first_bound {d : ℕ} {eps : ℝ} {oracle : PairOracle d} {report : TrialReport d} {p M D : ℝ} {x0 : Point d} {m₁ m₂ : ℕ} (hp : 1 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (hshape : FullShape p eps M D x0 oracle report m₁ m₂) : ↑report.calls ≤ 4 * √(M * D / ((p - 1) * eps)) + 2

theorem V7.Stage3BelowTwoS3F.first_to_second_bound {eps p M D : ℝ} (hp : 1 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (hkappa : 1 ≤ M * D / eps) : 4 * √(M * D / ((p - 1) * eps)) + 2 ≤ (4 / √(p - 1) + 2) * √(M * D / eps)