computable_add
plain-language theorem explainer
Computable reals are closed under addition. Researchers confirming that Recognition Science constants remain algorithmically approximable cite this result when combining sums of derived quantities. The tactic proof extracts the two witness sequences, shifts their indices by one step to absorb the doubled error, and closes the bound via the triangle inequality together with a power-of-two reduction identity.
Claim. If real numbers $x$ and $y$ each admit a sequence of rationals converging at rate $2^{-n}$, then their sum $x+y$ admits such a sequence. Here a real is computable precisely when there exists a map $f:ℕ→ℚ$ satisfying $|x-f(n)|<2^{-n}$ for every natural number $n$.
background
The module resolves the classical-versus-constructive objection by separating proof logic from output computability: classical steps in Lean do not prevent the derived constants from being algorithmically approximable. The Computable class, defined locally, asserts exactly that an approximating function to rationals exists with error strictly less than $2^{-n}$. The upstream computable_neg result shows the same closure under negation by pointwise negation of the witness sequence.
proof idea
Obtain the witness sequences $f$ and $g$ from the two hypotheses. Define the combined approximant by evaluating both at input $n+1$ and adding. Bound the error first by the triangle inequality, then add the two strict inequalities, and finally reduce twice the $n+1$ error to the target $n$ error via ring and zpow arithmetic. The final linarith step discharges the resulting inequality.
why it matters
The result is invoked directly by the downstream computable_sub theorem, which reduces subtraction to addition after negation. It thereby completes the basic arithmetic closure needed to confirm that all constants generated by the phi-ladder and the forcing chain (T5–T8) remain computable reals, supporting the module’s claim that Recognition Science outputs are algorithmically accessible irrespective of classical proof machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.