computable_sub
plain-language theorem explainer
Computable reals are closed under subtraction. Researchers checking that Recognition Science constants remain algorithmically approximable would cite this closure when confirming field operations preserve computability. The proof obtains the negation of the second argument, adds it to the first via the addition closure, and rewrites the difference through a ring identity.
Claim. If the real numbers $x$ and $y$ admit algorithms that approximate them by rationals to arbitrary precision, then their difference admits such an algorithm.
background
The module separates proof machinery from output computability: classical logic in Lean proofs does not affect whether derived constants admit algorithmic approximations. A real number is computable precisely when there exists a map from natural numbers to rationals satisfying the error bound $2^{-n}$ for every precision level. This theorem belongs to the sequence establishing that the computable reals are closed under arithmetic operations.
proof idea
The tactic proof first invokes the negation closure on the second hypothesis to obtain computability of the additive inverse. It then applies the addition closure to the original first argument and the negated second argument. A ring rewrite equates the difference to this sum, after which the addition result is used directly.
why it matters
The result supports the module's resolution of the classical-constructive objection by confirming that subtraction preserves algorithmic approximability of outputs. It forms part of the arithmetic closure chain alongside the negation and addition lemmas, reinforcing that constants such as phi and pi remain computable regardless of the logic used in their derivations. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.