computable_div
plain-language theorem explainer
If two real numbers admit algorithmic rational approximations to any precision and the divisor is nonzero, their quotient also admits such approximations. Researchers confirming that Recognition Science constants remain algorithmically definable would cite the closure. The argument reduces at once to a preexisting global instance of the approximation predicate.
Claim. Let $x,y$ be real numbers such that there exist sequences of rationals $f,g$ with $|x-f(n)|<2^{-n}$ and $|y-g(n)|<2^{-n}$ for all $n$, and let $y≠0$. Then there exists a sequence of rationals $h$ with $|x/y-h(n)|<2^{-n}$ for all $n$.
background
The module separates proof machinery from output computability: classical logic in derivations does not prevent the final constants from satisfying an algorithmic approximation criterion. A real number is computable precisely when an algorithm exists that, on input $n$, returns a rational within distance $2^{-n}$. The same predicate appears in the sibling multiplication closure, which likewise appeals to a global instance after recalling the standard error bound $|xy-f(k)g(k)|≤|x||y-g(k)|+|g(k)||x-f(k)|.
proof idea
The proof is a one-line term that invokes infer_instance. It relies on the upstream multiplication closure only indirectly through the shared instance mechanism and on the PrimitiveDistinction axioms for the ambient real field.
why it matters
The result supplies the division step needed for the curvature term 103/(102π^5) to be shown computable in the downstream theorem. It directly supports the module's resolution that derived constants (including those built from π and φ) remain inside the computable reals even when proofs use classical logic. This closes one concrete instance of the classical-constructive gap identified in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.