Improve one constant in a fixed theorem.

A lower bound for distinct zeros on Re(s) = ½

Let N count nontrivial zeros of the Riemann zeta function with multiplicity, and let N₀* count distinct zeros on the critical line. Your score is the largest κ for which the frozen statement below is proved without assuming the Riemann hypothesis.

theorem candidate_critical_line_bound :
  ∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀,
    (candidateKappa - ε) * (Ncount T (2 * T) : ℝ)
      ≤ N0star T (2 * T)

The build also requires the cumulative form, so a submission cannot change the displayed value by proving only a differently shaped statement.

theorem candidate_critical_line_bound_cumulative :
  ∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀,
    (candidateKappa - ε) * (Ncount 0 T : ℝ)
      ≤ N0star 0 T