AlphaPrecisionCert
plain-language theorem explainer
AlphaPrecisionCert packages the geometric seed equality to 4π×11, seed positivity, curvature correction positivity, and gap correction positivity into a single certificate. A physicist deriving the fine-structure constant in Recognition Science would cite it to support the 60 ppm interval claim for α⁻¹. The structure is assembled by a constructor that invokes the four supporting lemmas without further reduction.
Claim. The structure certifies that the geometric seed satisfies $α_{seed} = 4π × 11$, that $0 < α_{seed}$, that the curvature correction $δ_κ = φ^{-5}$ is positive, and that the gap correction $δ_g(w,s) = s exp(-w ln φ / s)$ is positive whenever $w > 0$ and $s > 0$.
background
In the Alpha-Inverse Precision Refinement module the inverse fine-structure constant is built from an additive geometric seed and an exponential resummation. The seed is defined as $4π × 11$, representing the baseline spherical closure cost over 11-edge interaction paths. The curvature correction is $φ^{-5}$ and the gap correction is the function $s exp(-w ln φ / s)$ for weight $w$ and seed $s$ (see upstream alpha_seed in Constants.Alpha and the local definitions of curvature_correction and gap_correction).
proof idea
This declaration is a pure structure definition that packages four field assertions. No tactics or lemmas are applied inside the structure itself; the fields are populated downstream by the theorem that constructs a witness from the seed-equality, seed-positivity, curvature-positivity, and gap-positivity lemmas.
why it matters
AlphaPrecisionCert supplies the certificate required to establish existence of a structure witnessing the precision bounds on α⁻¹. It fills the Q8 refinement step in the Recognition Science derivation of constants, where the alpha band (137.030, 137.039) is obtained from the geometric seed 4π×11 together with curvature and gap corrections. The construction relies on the phi-ladder from the forcing chain, though higher-order terms remain open for 1 ppm accuracy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.