Computable
plain-language theorem explainer
A real number x is computable when a sequence of rationals approximates it to precision 2^{-n} for each n. Researchers establishing algorithmic outputs for Recognition Science constants cite this predicate to separate proof machinery from derived-value computability. The declaration is a direct class definition that packages the existence witness without further reduction.
Claim. A real number $x$ is computable if there exists a function $f : ℕ → ℚ$ such that $|x - f(n)| < 2^{-n}$ for every natural number $n$.
background
The module resolves the objection that classical axioms in Lean undermine Recognition Science's algorithmic claims. It separates proof logic from output computability: constants such as π and φ remain approximable by rationals even when their supporting theorems use classical choice. The definition formalizes this via an existence witness for fast rational approximations, independent of how the real is constructed upstream.
proof idea
This is the base class definition; the approx field directly encodes the predicate. No lemmas are applied because the declaration introduces the property rather than deriving it from prior results.
why it matters
The predicate feeds theorems that the discrete ledger state space has cardinality 2^8 and that phase functions on the eight-tick space are finite in number. It also supports the result that the geometric seed 4π·11 for α^{-1} is computable. The declaration closes the classical-constructive gap noted in the module while preserving the framework's claim that RS outputs lie in the computable reals, consistent with the eight-tick octave and Church-Turing structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.