computable_pow
If a real x is computable then x raised to any natural power remains computable. Workers verifying the algorithmic status of Recognition Science constants cite this to confirm that terms such as pi^5 in curvature expressions stay approximable by rationals. The argument is a direct induction on the exponent that reduces the base case to the computability of 1 and the inductive step to multiplication closure.
claimIf a real number $x$ is computable, then $x^n$ is computable for every natural number $n$.
background
The Computable class states that a real admits an algorithm producing rationals within $2^{-n}$ for each precision $n$. This module examines the distinction between classical proof machinery and the computability of output constants, noting that derived RS quantities such as pi, phi, and alpha inverse remain algorithmically approximable even when proofs invoke classical logic. The result relies on the sibling closure of computable reals under multiplication together with the successor structure on naturals.
proof idea
Induction on the exponent n. The zero case rewrites the power to 1 and obtains computability by casting the natural number 1. The successor case applies the power successor identity and invokes the multiplication closure on the inductive hypothesis and the original x.
why it matters in Recognition Science
The lemma is called by curvature_computable to discharge the pi^5 factor in the curvature term 103/(102 pi^5). It supplies one concrete instance of the module's claim that RS constants remain computable outputs, consistent with the phi-ladder mass formulas and the alpha band. No scaffolding or open discharge remains.
scope and limits
- Does not claim the Lean proof extracts to a certified program.
- Does not supply an explicit approximation algorithm.
- Does not extend to real exponents or non-positive bases.
Lean usage
have hpi5 : Computable (Real.pi ^ 5) := computable_pow hpi 5formal statement (Lean)
237theorem computable_pow {x : ℝ} (hx : Computable x) (n : ℕ) :
238 Computable (x ^ n) := by
proof body
Term-mode proof.
239 induction n with
240 | zero =>
241 simp only [pow_zero]
242 -- 1 is computable as a natural number
243 have h : Computable ((1 : ℕ) : ℝ) := inferInstance
244 simp only [Nat.cast_one] at h
245 exact h
246 | succ n ih =>
247 simp only [pow_succ]
248 exact computable_mul ih hx
249
250/-- ln is computable on positive reals.
251
252 **Proof approach**: Use argument reduction + Taylor series.
253 1. Find k such that x·2^(-k) ∈ [1/2, 2] (k = ⌊log₂(x)⌋)
254 2. Let y = x·2^(-k), so log(x) = log(y) + k·log(2)
255 3. Use log(y) = 2·arctanh((y-1)/(y+1)) for y ∈ [1/2, 2]
256 4. arctanh(z) = z + z³/3 + z⁵/5 + ... converges for |z| < 1
257
258 For y ∈ [1/2, 2], we have |(y-1)/(y+1)| ≤ 1/3, giving fast convergence.
259
260 **Status**: Axiom (Taylor series algorithm) -/