candidate_2_value
plain-language theorem explainer
The second geometric candidate for the α⁻¹ correction equals exactly 1/824. Anyone comparing cube-geometry ansätze against the ~0.00110 gap between α⁻¹_RS and CODATA cites this identity. The proof is a one-line unfold-and-normalize: simplify the definition and discharge the rational equality by norm_num.
Claim. The second candidate correction term equals $1/824$ exactly (numerically $\approx 0.001214$).
background
The module studies the 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 the CODATA anchor $137.035999206(21)$. The required additive correction is $\delta_2 \approx +0.00110$.
Admissible corrections must be built from counting-layer integers and the fixed transcendentals $\pi,\varphi$, stay $O(10^{-3})$, introduce no free parameters, and admit a cube-geometry reading. Several closed-form candidates are defined and scored against that target.
Candidate 2 is the pure reciprocal integer $1/824$. Sibling material records that it sits ~10% above $\delta_2$, while candidate 1 ($1/(102\pi^2)$) sits ~10% below, so the target lies strictly between them.
proof idea
Term-mode proof in two tactics. First simp [candidate_2] unfolds the definition of the candidate to the literal rational $1/824$. Then norm_num closes the equality of rationals. No external lemmas are required beyond the definition itself.
why it matters
Inside the alpha-correction analysis this pins the exact closed form of the second counting-layer ansatz, so numerical comparisons ("~10% high") rest on a proved identity rather than a floating evaluation. The module's structural note places $\delta_2$ between candidate 1 ($1/(102\pi^2)$) and this value, and records that no single counting-layer expression hits the target exactly without a free weight.
That honesty matters for the RS alpha band: the seed formula already lands inside $(137.030, 137.039)$, and $\delta_2$ is the residual after the curvature term $103/(102\pi^5)$. The result does not yet feed a parent theorem (no downstream uses), but it is the certified value any later weighted combination or QED-vacuum comparison must quote. Framework context: $\varphi$ and the eight-tick / cube counting layer constrain which integers (here 824) are admissible under (A1)–(A4).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.