err_isBigO
plain-language theorem explainer
The declaration asserts that the specific error term x to the power 1/2 times (1 plus half log x) cubed is big-O of x over log x at infinity, conditional on the same relation. Number theorists applying explicit bounds to the prime counting function would cite this when controlling remainders in estimates derived from Brun-Titchmarsh. The proof is a one-line wrapper that introduces the hypothesis and matches it exactly to the goal.
Claim. Let $E(x) = x^{1/2} (1 + (1/2) log x)^3$. If $E(x) = O(x / log x)$ as $x → ∞$, then the same big-O relation holds.
background
The module ports results related to the Brun-Titchmarsh theorem into the Recognition Science setting, focusing on asymptotic bounds for primes. It relies on Mathlib's big-O notation with the atTop filter to express limits as x tends to infinity. The error term E(x) arises in explicit versions of the prime counting function π(x), where the main term is x / log x and the remainder must be controlled for applications to the phi-ladder mass formulas.
proof idea
The proof is a one-line wrapper that applies the hypothesis directly: introduce the assumption hErr, then use exact to discharge the identical goal.
why it matters
This names the error bound for the prime counting function, supporting downstream explicit estimates such as those in sibling declarations for card_range_filter_prime_isBigO and prime_counting_explicit_bound. In the Recognition framework it supplies the number-theoretic control needed for the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder, though no direct used_by edges are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.