computable_neg
plain-language theorem explainer
If a real number x admits a sequence of rational approximations f(n) with |x - f(n)| < 2^{-n} for each n, then -x admits the negated sequence with the same error bound. Researchers establishing closure of computable reals under arithmetic operations in the Recognition Science setting would cite this result. The proof extracts the witness function from the hypothesis and verifies the error equality via ring simplification and the absolute-value negation identity.
Claim. Let $x$ be a real number. If there exists a function $f : ℕ → ℚ$ such that $|x - f(n)| < 2^{-n}$ for every natural number $n$, then there exists a function $g$ such that $|-x - g(n)| < 2^{-n}$ for every $n$.
background
The module examines the distinction between classical reasoning used in proofs and the computability of constants derived in Recognition Science. A real number is computable precisely when an algorithm exists that, given any natural number $n$, returns a rational $q$ satisfying $|x - q| < 2^{-n}$. This definition appears as the Computable class whose witness is an existential quantifier over approximation functions. The present theorem is the first step in showing that the computable reals form a field under the usual operations.
proof idea
The tactic proof obtains the approximation witness ⟨f, hf⟩ from the hypothesis that x is computable. It constructs the new witness by sending each n to -f n, then applies ring_nf to rewrite the error expression and invokes abs_neg to equate |-(x - f n)| with |x - f n|, which is already bounded by the original hypothesis.
why it matters
This closure result under negation is invoked directly by the downstream theorems computable_sub and, indirectly, computable_add. It supports the module's resolution of the classical-versus-constructive objection by demonstrating that basic arithmetic operations preserve algorithmic approximability, thereby confirming that Recognition Science constants such as φ and α^{-1} remain computable regardless of the classical logic employed in their derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.