The irrationality measure of π is at most 19.8899945

Theorem PiIrrationality.chudnovsky_bound asserts that the real number $B = 19.8899945$ satisfies the property PiIrrationality.UpperBound. The decimal literal is interpreted as the exact rational real number $\frac{198899945}{10^{7}}$ $= \frac{39779989}{2000000}$ (no floating-point rounding). Unfolding the definition, the statement is:

For every real number $\varepsilon > 0$ there exists a natural number $Q \in \mathbb{N} = \{0,1,2,\dots\}$ such that for every integer $p \in \mathbb{Z}$ and every natural number $q$ with $q > 0$ and $q \ge Q$,

Here $\pi$ is the real constant Real.pi, $p$ and $q$ are cast to real numbers, $p/q$ is real division (well-defined since $q \ge 1$), $|\cdot|$ is the real absolute value, and the power $q^{19.8899945 + \varepsilon}$ is the real-exponent power function Real.rpow (for the positive base $q$ this is $\exp((19.8899945 + \varepsilon)\ln q)$, the usual real power). The inequality is strict. The threshold $Q$ may depend on $\varepsilon$ but not on $p$ or $q$; it is allowed to be $0$ or $1$, in which case the only constraint on $q$ is $q \ge 1$. The integer $p$ is unrestricted (any sign, including $0$), and there is no requirement that $p$ and $q$ be coprime or that $p/q$ be close to $\pi$; for fractions far from $\pi$ the inequality is easy, so the content concerns approximations near $\pi$. No other hypotheses, implicit arguments, or typeclass assumptions appear.