alpha_inv_formula
plain-language theorem explainer
The declaration defines the inverse fine-structure constant as the sum of a geometric seed term and a curvature correction. Researchers deriving constants from the Recognition Science framework cite it when assembling the final step of the φ-to-α⁻¹ chain. The definition is a direct one-line addition of the two supplied real parameters.
Claim. The inverse fine-structure constant is given by $α^{-1} = s + c$, where $s$ is the geometric seed $128 · ln(π/2) + 45 · ln φ$ and $c$ is the curvature correction term (approximately 0.05).
background
The RRF module derives all constants from φ via the chain φ → E_coh → τ₀ → c → ℏ → G → α⁻¹. The geometric seed is supplied by the sibling definition geometric_seed := 128 * Real.log (Real.pi / 2) + 45 * Real.log phi, whose doc-comment states it yields α⁻¹ ≈ 137.036. Upstream geometric_seed definitions supply the factors: one from Q₃ geometry as Ω(∂Q₃) × E_passive with 4π·11, another as the D=3 ratio 11/16.
proof idea
This is a one-line definition that adds the geometric seed parameter to the curvature correction parameter.
why it matters
It supplies the explicit formula for α⁻¹ in the derivation chain, placing the result inside the framework interval (137.030, 137.039). The declaration closes the constants sequence begun by the geometric_seed definitions and the module's gate identities (IR Gate, Planck Gate, K-Gates). No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.