alphaProvenance_inhabited
plain-language theorem explainer
The theorem asserts existence of a structural certificate confirming the inverse fine-structure constant lies in the Recognition Science band. Researchers tracing the provenance from J-uniqueness through the phi fixed point and D=3 to the explicit alpha formula would cite this result. The proof is a one-line term that supplies the explicit certificate construction as witness.
Claim. There exists a structural certificate witnessing that the CODATA value of the inverse fine-structure constant lies strictly between the Recognition Science lower and upper bounds, that the golden ratio equals $(1 + √5)/2$, that this ratio exceeds 1, and that the threshold $φ - 3/2$ is positive.
background
The module supplies an explicit chain from the J-uniqueness theorem to the fine-structure constant. The chain begins with the uniqueness result that forces $J(x) = (x + x^{-1})/2 - 1$, proceeds through the self-similar fixed point $φ$, derives three spatial dimensions from the eight-tick period, assembles a 44-slot frequency structure, and arrives at the formula $α^{-1} = 44π exp(-8 ln φ / (44π))$, whose numerical value is verified to lie inside the CODATA interval (137.030, 137.039).
proof idea
The proof is a one-line term-mode wrapper. It directly constructs an inhabitant of Nonempty AlphaProvenanceCert by supplying the witness produced by the sibling definition alphaProvenanceCert, whose fields are filled by the codata band membership predicate together with the golden-ratio identity and two linarith applications for the strict inequalities.
why it matters
The declaration closes the structural provenance chain listed in the module documentation, confirming that every step from washburn_uniqueness_aczel through phi_fixed_point and the D=3 forcing lands on an inhabited certificate. It thereby supports the explicit alpha derivation that places the CODATA value inside the predicted band and links the T5 J-uniqueness and T6 phi fixed-point landmarks to a concrete numerical check. No downstream uses are recorded, so the result functions as a terminal verification node in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Gravitational polarization leaves sigma8 tension unchanged
"Eq.(3) implies that gravitational particle production has a significant contribution to the effective Hubble parameter if sum (mi c2/eV)^2 is not extremely smaller than 10^58"
-
Z to mu mu b b decay gives first limits on muon-bottom SMEFT operators
"The resulting 95% C.L. intervals on the WCs obtained from this procedure are summarized in Table IV."