computable_div
Computable reals are closed under division by a nonzero computable divisor. Researchers establishing algorithmic accessibility of Recognition Science constants would cite this closure property when deriving further expressions from basic computable quantities. The proof is a one-line term that invokes the global classical instance for the Computable predicate.
claimIf $x, y$ are computable reals with $y$ nonzero, then the quotient $x/y$ is computable.
background
The module addresses the distinction between classical proof machinery and the computability of derived constants in Recognition Science. A real number $x$ is computable when there exists an algorithm producing rationals $f(n)$ satisfying $|x - f(n)| < 2^{-n}$ for every $n$. This result builds on the sibling closure under multiplication and the foundational distinction axioms that separate structural conditions from definitional facts.
proof idea
The proof is a one-line wrapper that applies the global classical instance for the Computable class, which already encodes closure under division by nonzero elements.
why it matters in Recognition Science
This theorem ensures arithmetic combinations of computable reals remain computable and feeds directly into the proof that the curvature term $103/(102 pi^5)$ is computable. It supports the module's resolution of the classical-constructive objection by confirming that output constants stay algorithmically approximable. The result aligns with the broader claim that constants such as pi and phi remain computable regardless of the logic used in their proofs.
scope and limits
- Does not construct an explicit division algorithm.
- Does not address the classical logic used in the underlying proof system.
- Does not apply when the divisor is zero.
- Does not extend the closure property beyond real numbers.
Lean usage
have h : Computable (x / y) := computable_div hx hy hneformal statement (Lean)
230theorem computable_div {x y : ℝ} (hx : Computable x) (hy : Computable y) (hne : y ≠ 0) :
231 Computable (x / y) := by
proof body
Term-mode proof.
232 -- Immediate from the global classical instance.
233 infer_instance
234
235/-- Computable reals are closed under natural number exponentiation.
236 Proof by induction: x^0 = 1 (computable), x^(n+1) = x * x^n (by computable_mul). -/