pi_computable
plain-language theorem explainer
The theorem asserts that π satisfies the Computable predicate, so rational approximations exist to any dyadic precision. Recognition Science authors cite it when confirming that constants entering the fine-structure expression remain algorithmically accessible despite classical proof steps. The proof is a one-line wrapper invoking the Mathlib typeclass instance for π.
Claim. The real number π is computable: there exists a function $f : ℕ → ℚ$ such that $|π - f(n)| < 2^{-n}$ for every natural number $n$.
background
The module examines the distinction between classical proof machinery and the computability of derived outputs in Recognition Science. The Computable class encodes the existence of an algorithm that, on input n, returns a rational within 2^{-n} of the target real. The local setting stresses that classical logic in proofs does not alter whether specific constants admit such approximations. Upstream results on mass-to-light ratios and simplicial ledger bridges supply context for why computable constants matter downstream, but supply no direct lemmas here.
proof idea
The proof is a one-line wrapper that applies the existing Mathlib instance for the Computable class on Real.pi.
why it matters
This result supplies the base case for two immediate applications: the geometric seed 4π·11 and the curvature term 103/(102 π^5) are shown computable by composing with the operations in the same file. It directly supports the module's resolution of the classical-versus-constructive objection by separating proof style from output accessibility. Within the framework it anchors the claim that constants such as those appearing in the alpha band remain algorithmically accessible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.