The irrationality measure of π is at most 14.797074

The declaration asserts that the real number $B = 14.797074$ satisfies the property UpperBound (in the namespace PiIrrationality), where the decimal literal is read as the exact rational real number $B = \frac{14797074}{1000000} = \frac{7398537}{500000}$ (not a floating-point approximation). The theorem takes no hypotheses or arguments. Unfolding the definition, the statement says: for every real $\varepsilon > 0$ there exists a natural number $Q \ge 0$ such that for every integer $p \in \mathbb{Z}$ and every natural number $q$ with $q > 0$ and $q \ge Q$,

where $\pi$ is the real constant $\pi$, $p/q$ is ordinary real division (well-defined since $q \ge 1$), $|\cdot|$ is the real absolute value, and $q^{B+\varepsilon}$ is the real power $q^{x} = \exp(x \ln q)$ of the positive real $q$ to the real exponent $x = B + \varepsilon = 14.797074 + \varepsilon$. Points to note: the inequality is strict; $Q$ may depend on $\varepsilon$ (but not on $p$ or $q$), so only the finitely many denominators $q < Q$ are exempt and nothing is claimed about them; $p$ ranges over all integers, $p/q$ need not be in lowest terms, and $q = 0$ is excluded by the hypothesis $q > 0$; the case $q = 1$ is covered whenever $Q \le 1$, in which case the claim reads $1 < |\pi - p|$ for all integers $p$. In words: for every $\varepsilon > 0$, every rational approximation $p/q$ to $\pi$ with sufficiently large denominator $q$ satisfies $|\pi - p/q| > q^{-(14.797074 + \varepsilon)}$.