curvature_computable
plain-language theorem explainer
The theorem shows that the curvature term 103/(102 π^5) satisfies the definition of a computable real. Workers on Recognition Science foundations cite it when separating proof machinery from output computability. The tactic proof composes the pi_computable instance with the computable_pow, computable_mul, and computable_div lemmas while discharging the nonzero denominator condition.
Claim. The real number $103/(102 π^5)$ is computable, i.e., there exists a function $f:ℕ→ℚ$ such that $|103/(102 π^5) - f(n)| < 2^{-n}$ for every natural number $n$.
background
The module ConstructiveNote resolves Gap 2 by distinguishing proof logic from the computability of derived constants. A real is computable when an algorithm exists that, given precision parameter n, returns a rational within 2^{-n}. The module states that π remains computable despite classical reasoning in its proofs, and the same holds for RS constants such as the curvature term. Upstream results supply the supporting computability instances for π and the arithmetic operations on reals.
proof idea
The tactic proof first obtains computability of the integer literals 103 and 102 via inferInstance, then invokes pi_computable to obtain computability of π. It applies computable_pow to reach π^5, computable_mul to form the denominator, proves the denominator is nonzero by mul_ne_zero and pow_ne_zero, and finally applies computable_div to conclude.
why it matters
This declaration belongs to the ConstructiveNote module that closes the classical-versus-constructive objection for Recognition Science. It demonstrates that a concrete derived constant appearing in curvature expressions is computable, consistent with the module's claim that all RS-derived constants (including those inside the alpha band) remain algorithmically approximable. No downstream theorems are recorded, so the result functions as a self-contained clarification rather than a lemma in a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.