log_alphaInv_eq
plain-language theorem explainer
The theorem establishes the logarithmic identity ln(α⁻¹) = ln(α_seed) − f_gap/α_seed for the inverse fine-structure constant. Researchers deriving α from Recognition Science structures cite it to confirm consistency of the exponential representation. The proof reduces the claim to a prior ratio identity by applying the logarithm division rule and linear arithmetic.
Claim. $ln(α^{-1}) = ln(α_{seed}) - f_{gap}/α_{seed}$
background
The AlphaExponentialForm module examines structural properties of the exponential representation α⁻¹ = α_seed ⋅ exp(−f_gap/α_seed). Here α_seed = 4π⋅11 is the geometric seed from ledger structure, and f_gap encodes the gap weight w₈ ln(φ) on the phi-ladder. The module proves positivity of α⁻¹ and identifies the ODE d(α⁻¹)/d(f_gap) = −α⁻¹/α_seed satisfied by the form, analogous to renormalization-group equations for a running coupling with α_seed as scale.
proof idea
The proof invokes the upstream result log_alphaInv_seed_ratio, which states that the log of the ratio alphaInv/alpha_seed equals −f_gap/alpha_seed. It rewrites this using Real.log_div, justified by the positivity of alphaInv and alpha_seed, then applies linear arithmetic to obtain the difference of logs.
why it matters
This identity feeds the downstream theorem exponential_form_uniqueness_ode_principle, which notes that constant logarithmic derivative characterizes the exponential family via standard ODE theory. It addresses Gap B in the validation program for the canonical alpha formula, as described in the module documentation. The form is motivated by J-cost log-structure, though the physical reason for constant log derivative in RS remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.