log_alphaInv_seed_ratio
plain-language theorem explainer
The theorem states that the natural log of the ratio of the inverse fine-structure constant to its geometric seed equals the negative of the gap weight divided by the seed. Researchers deriving logarithmic relations or ODE properties for alpha in the Recognition Science constants pipeline would cite it. The proof is a one-line wrapper that substitutes the exponential ratio identity and applies the log-of-exp cancellation.
Claim. $ln(alpha^{-1}/alpha_seed) = -f_gap/alpha_seed$, where $alpha^{-1}$ is the inverse fine-structure constant obtained from the exponential resummation $alpha_seed * exp(-f_gap/alpha_seed)$, $alpha_seed = 4 pi * 11$, and $f_gap$ is the gap weight $w_8 ln phi$.
background
The AlphaExponentialForm module examines the canonical expression $alpha^{-1} = alpha_seed * exp(-f_gap/alpha_seed)$, where $alpha_seed = 4 * pi * 11$ is the geometric seed from ledger structure representing baseline spherical closure cost over 11-edge paths, and $f_gap = w_8 * ln phi$ is the gap weight from the DFT-8 projection. The upstream theorem alphaInv_seed_ratio establishes that the ratio $alphaInv/alpha_seed$ equals exactly the exponential factor $exp(-f_gap/alpha_seed)$. This log theorem converts that multiplicative relation into an additive one on the log scale, consistent with the module's focus on positivity, logarithmic derivatives, and the structural motivation from J-cost log-coordinate expansions.
proof idea
The proof is a one-line wrapper that first rewrites the left-hand side via the alphaInv_seed_ratio theorem to obtain log(exp(-f_gap/alpha_seed)), then applies the lemma Real.log_exp to cancel the logarithm and exponential, yielding the right-hand side directly.
why it matters
It feeds directly into the downstream theorem log_alphaInv_eq, which rewrites ln(alphaInv) as ln(alpha_seed) minus f_gap/alpha_seed, and supports the exponential_form_uniqueness_ode_principle analysis of the logarithmic ODE satisfied by alpha^{-1}. In the Recognition Science framework this confirms the exponential form's compatibility with running-coupling behavior and the J-cost log-structure, while the module explicitly flags that uniqueness of the exponential Taylor coefficients from first principles remains an open BRIDGE claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.