alphaInvValue
plain-language theorem explainer
This definition supplies the string representation of the inverse fine-structure constant assembled from the Recognition Science curvature pipeline. Researchers generating deterministic audit reports for unitless invariants would cite it when populating the JSON summary. The implementation is a direct alias to the upstream numeric evaluator that assembles the rational approximations for π, φ, and the gap correction terms.
Claim. $α^{-1} ≈ 4π·11 − (w_8 ln φ + δ_κ)$ with π ≈ 104348/33215, φ ≈ 161803399/100000000, w_8 ≈ 2.488254397846, and δ_κ = −103/(102 π^5).
background
The Audit module supplies scaffolding for emitting a deterministic JSON summary of already-proven unitless invariants under the Recognition Science framework. It imports the numeric generator module to obtain the fine-structure value. The upstream alphaInvValueStr evaluates α^{-1} ≈ 4π·11 − (w_8·ln φ + δ_κ) using the stated high-precision rationals and the alternating series for ln φ.
proof idea
One-line wrapper that directly returns the string produced by alphaInvValueStr.
why it matters
This definition supplies the alpha inverse string for the audit report surface, feeding the list of proven invariants that includes EightTickMinimality and UnitsInvariance. It realizes the alpha band prediction (137.030, 137.039) that follows from T5 J-uniqueness and T6 phi fixed point in the forcing chain. The value closes the numeric evaluation step for the curvature terms before later milestones add scale dependence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.