computable_sub
Computable reals are closed under subtraction. Researchers verifying the algorithmic character of Recognition Science constants would cite this to confirm that differences of computable quantities remain computable. The proof is a short tactic sequence that invokes the negation and addition lemmas after rewriting the difference via the ring identity x - y = x + (-y).
claimLet $x, y$ be real numbers each admitting an algorithm that, for every precision $n$, outputs a rational within distance $2^{-n}$. Then $x - y$ admits such an algorithm.
background
The module addresses the distinction between classical proof machinery and the computability of derived constants in Recognition Science. A real number is computable when an algorithm exists that, for any precision $n$, produces a rational within $2^{-n}$ of the target. This theorem belongs to a suite establishing that the computable reals are closed under the field operations, supporting the claim that constants such as phi and pi remain computable regardless of the logic used in their proofs.
proof idea
The proof first applies the negation lemma to obtain computability of -y. It then invokes the addition lemma on x and -y. A ring tactic rewrites the subtraction as addition of the negation, after which the result follows directly by exact matching.
why it matters in Recognition Science
This result contributes to the formal demonstration that the derived constants of Recognition Science are computable reals. It forms part of the constructive note module that resolves the apparent tension between classical Lean proofs and algorithmic foundations. The parent structure is the Computable class, and it aligns with the framework's emphasis on output computability over proof style.
scope and limits
- Does not establish computability of arbitrary real numbers.
- Does not resolve the use of classical axioms in the broader proof system.
- Does not provide explicit algorithms for subtraction.
- Does not apply outside the real numbers.
formal statement (Lean)
199theorem computable_sub {x y : ℝ} (hx : Computable x) (hy : Computable y) :
200 Computable (x - y) := by
proof body
Tactic-mode proof.
201 have hny : Computable (-y) := computable_neg hy
202 have h := computable_add hx hny
203 have heq : x - y = x + (-y) := by ring
204 rw [heq]
205 exact h
206
207/-- Computable reals are closed under multiplication.
208
209 Proof idea: |xy - f(k)g(k)| ≤ |x||y-g(k)| + |g(k)||x-f(k)|.
210 With bounds on |x|, |y| from initial approximations, we can compute
211 how much extra precision is needed.
212
213 The formal proof is complex but the mathematics is standard. -/