AlphaProvenanceCert
plain-language theorem explainer
AlphaProvenanceCert bundles the interval membership of the CODATA alpha inverse inside the RS band (137.030, 137.039) with the explicit golden-ratio definition of phi and the two positivity conditions on phi. A researcher closing the numerical step of an alpha derivation from the J-uniqueness theorem would cite this certificate to confirm the provenance chain reaches a verified band. The structure is populated by a direct construction that supplies the codata_in_band theorem together with linarith on the phi inequalities.
Claim. A structure whose fields assert $137.030 < 137.035999084 < 137.039$, the equality $phi = (1 + sqrt(5))/2$, the inequality $1 < phi$, and the inequality $0 < phi - 3/2$.
background
The module supplies an explicit derivation of the fine-structure constant from the recognition uniqueness theorem. alphaInverseLower and alphaInverseUpper are the constants 137.030 and 137.039 that bound the RS interval forced by the 44-pi formula. codataAlphaInverse is the CODATA 2022 value 137.035999084. The theorem codata_in_band establishes strict membership by norm_num. phi is the golden ratio arising as the unique self-similar fixed point of the J-cost functional equation J(x) = (x + x^{-1})/2 - 1.
proof idea
The declaration is a structure definition whose four fields are the required propositions. The codata_in_band field is filled by the theorem of the same name. The phi_is_golden field is the explicit equality, while phi_gt_one and threshold_pos are the two inequalities on phi. No tactics appear inside the structure; the concrete values are supplied by the downstream noncomputable definition alphaProvenanceCert.
why it matters
The certificate packages the final numerical check of the alpha provenance chain that begins with the J-uniqueness theorem, proceeds through the forced phi fixed point and D = 3, and arrives at the 44-slot structure whose formula yields alpha^{-1} inside (137.030, 137.039). It is consumed by alphaProvenanceCert and alphaProvenance_inhabited to witness that the chain is inhabited. In the Recognition framework this completes the explicit verification step linking T5 J-uniqueness and T6 phi to the observed alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Coupled PINN reconstructs greenhouse climate states and parameters
"(a₁..a₄)=(0.18,3.50,0.12,0.015), (b₁..b₄)=(0.12,5.00,0.08,0.06) ... 25% of grid retained, Gaussian noise σ=0.30 and 1.00 added."
-
Four-level atoms enable negative refraction with EIT-suppressed absorption
"Ω s=14γ, 18 γ, 20 γ correspond to the solid, dotted and dashed curves... The detuning of the strong signal field is set as ∆ s = 0, and ∆ c = ∆ m = 0 . 005γ. The phase difference ... θ= 1/6 π."