alpha_inv_formula
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the numerical value of the curvature correction term.
- Does not derive the geometric seed from Q₃ geometry or the 8-tick structure.
- Does not verify numerical agreement with the measured α⁻¹.
formal statement (Lean)
101noncomputable def alpha_inv_formula (geometric_seed curvature_corr : ℝ) : ℝ :=
proof body
Definition body.
102 geometric_seed + curvature_corr
103
104/-- The geometric seed: 128 · ln(π/2) + 45 · ln φ. -/