log_alphaInv_eq
plain-language theorem explainer
Recognition Science records the identity ln(α^{-1}) = ln(α_seed) - f_gap/α_seed for the exponential parameterization of the inverse fine-structure constant. Analysts of the alpha exponential form in the Constants module cite this relation when reducing logarithmic expressions. The proof is a one-line algebraic reduction that invokes the seed-ratio logarithm theorem, applies the division logarithm rule under positivity, and closes with linear arithmetic.
Claim. $ln(α^{-1}) = ln(α_seed) - f_gap / α_seed$
background
The module AlphaExponentialForm examines the canonical expression α^{-1} = α_seed · exp(-f_gap / α_seed) where α_seed = 4π·11 and f_gap = w_8 ln(φ). The definition alphaInv unfolds directly to this product. The upstream result log_alphaInv_seed_ratio states that Real.log (alphaInv / alpha_seed) = -(f_gap / alpha_seed), which is the immediate predecessor of the present identity.
proof idea
The term proof first obtains the ratio logarithm via log_alphaInv_seed_ratio. It rewrites the left-hand side using Real.log_div under the two positivity hypotheses alphaInv_positive and alpha_seed_positive. Linear arithmetic then equates the resulting expression to the target right-hand side.
why it matters
The identity supplies the logarithmic step required by the downstream theorem exponential_form_uniqueness_ode_principle, which records the ODE satisfied by the exponential form. It belongs to the structural analysis of the alpha band (α^{-1} inside (137.030, 137.039)) inside the Recognition Science constants pipeline. The module doc notes that the exponential form itself remains a bridge claim whose uniqueness from J-cost structure is not yet formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.