alpha_seed_computable
plain-language theorem explainer
The theorem shows that the real 4π·11 admits an algorithmic approximation to arbitrary precision. Workers on constructive foundations for Recognition Science cite it to verify that the geometric seed entering the inverse fine-structure constant remains computable. The term proof obtains instances for 4 and 11 by inferInstance, pulls the instance for π from pi_computable, and composes them under the multiplication closure of computable reals.
Claim. The real number $4π·11$ is computable: there exists a function $f:ℕ→ℚ$ such that $|4π·11-f(n)|<2^{-n}$ for every positive integer $n$.
background
The module ConstructiveNote resolves the objection that Recognition Science invokes classical axioms while claiming algorithmic foundations. It separates proof machinery (classical) from output computability (algorithmic). The class Computable(x:ℝ) asserts existence of an algorithm that, on input n, returns a rational q with |x-q|<2^{-n}. Upstream results supply the fact that π is computable and the theorem that computable reals are closed under multiplication.
proof idea
Term-mode proof. It obtains Computable instances for the naturals 4 and 11 by inferInstance, invokes pi_computable for π, simplifies the Nat.cast coercions, and applies the multiplication-closure theorem twice via computable_mul to reach the product.
why it matters
The declaration confirms that the geometric seed 4π·11 used for α^{-1} is computable, directly supporting the module's claim that derived constants remain algorithmically approximable. It aligns with the Recognition Science alpha band (137.030,137.039) and the broader emphasis on computable outputs. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.