curvature_computable
The real number 103 divided by 102 times pi to the fifth is shown to be computable. Researchers checking whether Recognition Science derived constants admit algorithmic approximation would cite the result. The tactic proof assembles the claim from the computability of pi together with closure of computable reals under multiplication, exponentiation, and division.
claimThe real number $103/(102 pi^5)$ is computable.
background
The module resolves the objection that Recognition Science relies on classical logic in Lean while claiming algorithmic foundations. The key distinction is between proof machinery, which may use classical steps, and the computability of derived constants, which must admit algorithmic approximation to arbitrary precision. A real number x is computable when there exists a function from naturals to rationals such that the approximation error is less than 2 to the minus n for each n. The module states that pi remains computable even though proofs about it employ classical logic, and the same holds for other RS constants built from arithmetic operations.
proof idea
The tactic proof obtains computability instances for the naturals 103 and 102 cast to reals, invokes the known computability of pi, applies the closure under exponentiation to obtain pi to the fifth, multiplies by 102, proves the denominator nonzero via norm_num and pow_ne_zero, and concludes with the division closure lemma.
why it matters in Recognition Science
This theorem supports the formal resolution of Gap 2 by exhibiting a concrete derived constant as computable, reinforcing that RS algorithmic claims concern output values rather than proof style. It aligns with the module emphasis that constants involving pi are computable to arbitrary precision, consistent with the framework's treatment of RS-native units where c equals 1 and other quantities are expressed via phi and pi. No downstream uses are recorded, but the result contributes to verification that expressions such as those appearing in curvature or spectral terms remain algorithmically accessible.
scope and limits
- Does not claim the Lean proof itself is constructive.
- Does not compute a numerical approximation of the term.
- Does not address physical interpretation of the curvature expression.
- Does not extend to constants outside this specific rational multiple of pi to the fifth.
formal statement (Lean)
283theorem curvature_computable : Computable ((103 : ℝ) / (102 * Real.pi ^ 5)) := by
proof body
Tactic-mode proof.
284 have h103 : Computable ((103 : ℕ) : ℝ) := inferInstance
285 have h102 : Computable ((102 : ℕ) : ℝ) := inferInstance
286 simp only [Nat.cast_ofNat] at h103 h102
287 have hpi : Computable Real.pi := pi_computable
288 have hpi5 : Computable (Real.pi ^ 5) := computable_pow hpi 5
289 have hdenom : Computable (102 * Real.pi ^ 5) := computable_mul h102 hpi5
290 have hne : (102 : ℝ) * Real.pi ^ 5 ≠ 0 := by
291 apply mul_ne_zero
292 · norm_num
293 · exact pow_ne_zero 5 Real.pi_ne_zero
294 exact computable_div h103 hdenom hne
295
296/-! ## Summary -/
297
298/-- Gap 2 Resolution: Classical proofs ≠ non-computable outputs.
299
300 The "algorithmic" claim of RS is about the DERIVED CONSTANTS being computable,
301 not about the proof machinery being constructive.
302
303 - Lean's `classical` tactic: OK (doesn't affect output values)
304 - Lean's `noncomputable`: OK (Lean limitation, not Turing limitation)
305 - Using Real.pi: OK (π is computable)
306 - Using Classical.choice: OK (only in proofs, not in computed values)
307
308 The key test: Can you write a program to compute α⁻¹ to arbitrary precision?
309 Answer: YES. Therefore α⁻¹ is computable. QED. -/
310
311end ConstructiveNote
312end Meta
313end IndisputableMonolith