candidate_1
plain-language theorem explainer
Defines the first geometric candidate for the residual α⁻¹ correction as 1/(102 π²) ≈ 9.94×10⁻⁴. Analysts comparing cube-geometry corrections to the ~0.00110 gap between α⁻¹_RS and CODATA cite it. It is a pure arithmetic definition: seam denominator 102 times π squared in the denominator.
Claim. The first candidate residual correction is $\delta^{(1)} := \dfrac{1}{102\,\pi^{2}}$, i.e. one over (face count $\times$ wallpaper factor) times $\pi^{2}$, reusing the seam denominator $102$ from the existing curvature term but with $\pi^{2}$ instead of $\pi^{5}$.
background
The module studies the ~0.001 residual needed to close the 8 ppm gap between the Recognition Science inverse fine-structure value $\alpha^{-1}_{\mathrm{RS}} = 4\pi\cdot 11 - w_8\ln\varphi + 103/(102\pi^5) \approx 137.0349$ and CODATA $137.035999206(21)$. The required additive shift is $\delta_2 \approx +0.00110$.
Admissible corrections must be built from counting-layer integers and the transcendentals $\pi,\varphi$, stay $O(10^{-3})$, introduce no free parameters, and admit a cube-geometry reading. The integer $102$ is the seam denominator for $D=3$; the related seam numerator is $102+1=103$ (base plus Euler closure), which already appears in the curvature term $103/(102\pi^5)$.
Candidate 1 keeps that same $102$ but replaces $\pi^5$ by $\pi^2$, interpreted as a lower-order curvature correction from face $\times$ wallpaper channels.
proof idea
Pure definition: the real constant is written as the reciprocal of $102$ times $\pi$ squared. No lemmas or tactics; downstream bounds unfold the definition and compare against decimal enclosures of $\pi$.
why it matters
Supplies the first explicit geometric ansatz in the candidate list for closing the $\alpha^{-1}$ gap. The immediate consumer is candidate_1_bounds, which proves $0.000993 < 1/(102\pi^2) < 0.000996$ and records that the value sits ~10% below the target $\delta_2\approx 0.00110$.
Within the Recognition framework this sits in the verification layer around the derived $\alpha$ band (primer: $\alpha^{-1}$ inside $(137.030,137.039)$). It tests whether a pure combinatorial factor times a lower power of $\pi$ can absorb the residual without new parameters, consistent with structural constraints (A1)–(A4). The analysis ultimately ranks several such candidates; this one is the face–wallpaper $\pi^2$ channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.