Level cap at BV level 1/2: log ratio below 1/4 - eta/2
Provedgpy_log_ratio_lt_bv_halfnumber-theory
Under the BV level constraint R^2 < Y'^(1/2 - eta), the log ratio log R / log Y' is below 1/4 - eta/2. This caps, but does not evaluate, the ratio's log factor; whether the cap 1/4 suffices depends on unevaluated inputs and is not decided here. Pure Mathlib statement.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_log_ratio_lt_bv_half {R Y' : ℕ} {η : ℝ}
(hR : 2 ≤ R) (hY : 1 < Y')
(hlev : (R : ℝ) ^ 2 < (Y' : ℝ) ^ (1 / 2 - η)) :
Real.log (R : ℝ) / Real.log (Y' : ℝ) < 1 / 4 - η / 2 := by sorrySource
GPY ratio analysis: threshold, main-term approximations, and BV level cap