computable_pow
plain-language theorem explainer
Natural number powers preserve computability for real numbers. Researchers verifying that Recognition Science constants remain algorithmically approximable would cite this closure result. The proof proceeds by induction on the exponent, with the base case using that 1 is computable and the successor case reducing directly to the already-established multiplication closure.
Claim. If a real number $x$ admits an algorithm producing rationals $q_n$ with $|x - q_n| < 2^{-n}$ for every $n$, then for every natural number $k$ the power $x^k$ admits such an algorithm.
background
The Computable class on reals requires an explicit approximation function from naturals to rationals meeting the $2^{-n}$ error bound. This module separates proof machinery (classical logic in Lean) from output computability of derived constants such as pi and phi. The local setting addresses the objection that classical axioms undermine constructive claims by showing that the distinction does not affect whether specific real values can be approximated algorithmically.
proof idea
Induction on the exponent n. The zero case invokes that the cast of 1 from Nat is computable by inferInstance, then rewrites via Nat.cast_one. The successor case rewrites via pow_succ and applies the sibling theorem computable_mul to the inductive hypothesis and the original hx.
why it matters
Supplies the exponentiation closure needed by curvature_computable to conclude that the term 103/(102 pi^5) is computable. This supports the module's resolution that RS constants (including those built from pi^5 in the alpha band) remain computable reals even when surrounding proofs use classical logic. It closes one step in the chain showing that derived quantities on the phi-ladder and in the eight-tick structure satisfy the algorithmic approximation criterion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.