candidate_2
plain-language theorem explainer
Defines the second geometric candidate for the fine-structure correction as 1/(8·103) = 1/824. Anyone comparing cube-geometry ansätze against the ~0.0011 gap between α⁻¹_RS and CODATA would cite it. The body is a pure real literal: vertices times the seam numerator in the denominator.
Claim. The second candidate correction is the real number $\delta^{(2)} := 1/(8 \cdot 103) = 1/824$, built from the cube's eight vertices and the seam numerator 103.
background
The module studies the residual ~8 ppm mismatch between the Recognition Science inverse fine-structure constant $\alpha^{-1}_{\mathrm{RS}} = 4\pi\cdot 11 - w_8\ln\varphi + 103/(102\pi^5) \approx 137.0349$ and the CODATA value $137.035999206(21)$. Closing the gap needs a positive additive correction $\delta_2 \approx +0.00110$ that obeys four structural constraints: counting-layer integers and transcendentals only, size $\sim 10^{-3}$, no free parameters, and a cube-geometry reading.
In the curvature-seam construction the denominator is faces times wallpaper groups ($6\times 17 = 102$ in $D=3$), while the numerator 103 appears in the existing $\alpha$ term. The cube also supplies eight vertices. Candidate 2 multiplies those two integers and inverts the product, reading the result as a vertex-level correction to the curvature seam.
Sibling candidates use other integer combinations (active edges, reduced $\pi^2$ factors, etc.); this one is the pure $V\times$ seam-numerator ansatz.
proof idea
Definitional abbreviation only: the real is written as the reciprocal of the product $8\cdot 103$. No lemmas are invoked. Downstream, candidate_2_value reduces it by simp and norm_num to the equal form $1/824$.
why it matters
Feeds the numerical evaluation theorem that records $\mathrm{candidate_2}=1/824\approx 0.001214$ and flags a ~10% overshoot relative to the target $\delta_2\approx 0.00110$. Inside the alpha-correction programme this is one of several cube-geometry expressions tested against constraints (A1)–(A4) before any term is admitted into the $\alpha^{-1}$ formula. The integers 8 and 103 sit next to the forced $D=3$ cube (T8) and the seam fraction already present in the RS seed; the candidate does not yet close the CODATA gap and remains an exploratory ansatz rather than a proved identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.