alpha_seed_computable
The result shows that the product 4π·11 admits an algorithmic approximation to arbitrary rational precision. Workers on constructive foundations for Recognition Science cite it to confirm that the geometric seed for the fine-structure constant remains computable even when classical logic is used in the surrounding proofs. The argument composes the known computability of π with the closure of computable reals under multiplication and the trivial computability of the integers 4 and 11.
claimThe real number $4π·11$ is computable: there exists a function $f:ℕ→ℚ$ such that $|4π·11 - f(n)| < 2^{-n}$ for every natural number $n$.
background
The module ConstructiveNote separates proof machinery from output computability. It notes that classical logic in Lean proofs does not prevent derived constants from being computable reals, where a real $x$ is computable when an algorithm produces rationals $f(n)$ satisfying $|x - f(n)| < 2^{-n}$ for all $n$. The sibling definition Computable encodes exactly this approximation property and records that π is computable via known series such as the Bailey-Borwein-Plouffe formula. Upstream results supply the closure of computable reals under multiplication (computable_mul) and the specific fact that π itself is computable (pi_computable).
proof idea
The term proof first obtains Computable instances for the constants 4 and 11 by inferInstance, then invokes pi_computable for the middle factor. After a simplification step that removes Nat.cast_ofNat, it applies the multiplication closure theorem twice: once to combine 4 with π and once to multiply the result by 11.
why it matters in Recognition Science
The declaration supplies one concrete instance of the module's general claim that RS-derived constants remain algorithmically accessible. It directly supports the computability of the seed 4π·11 that appears in the approximation α^{-1} ∈ (137.030, 137.039) and therefore contributes to the constructive side of the classical-versus-constructive debate recorded in the module documentation. No downstream theorems are listed, but the result closes a potential objection to the algorithmic character of the Recognition Science constants.
scope and limits
- Does not extract an explicit program from the proof.
- Does not assert computability of any other RS constant without separate argument.
- Does not claim that the surrounding classical logic can be replaced by constructive logic.
- Does not provide numerical bounds or convergence rates beyond the definition of Computable.
formal statement (Lean)
269theorem alpha_seed_computable : Computable (4 * Real.pi * 11) := by
proof body
Term-mode proof.
270 have h1 : Computable ((4 : ℕ) : ℝ) := inferInstance
271 have h2 : Computable Real.pi := pi_computable
272 have h3 : Computable ((11 : ℕ) : ℝ) := inferInstance
273 simp only [Nat.cast_ofNat] at h1 h3
274 exact computable_mul (computable_mul h1 h2) h3
275
276/-- ln φ is computable. -/