alphaInv_seed_ratio
plain-language theorem explainer
The ratio of the inverse fine-structure constant to its geometric seed equals the exponential suppression factor exp(-f_gap over alpha_seed). Researchers analyzing the canonical resummation of alpha inverse in Recognition Science would cite this identity when confirming the form alpha_seed times exp(-f_gap over alpha_seed). The proof is a direct unfolding of the alpha inverse definition followed by field simplification to cancel the common factor.
Claim. $ {a^{-1}} / {a_{seed}} = {exp}(-{f_{gap}} / {a_{seed}}) $
background
The module examines the exponential form posited for the inverse fine-structure constant: alpha inverse equals alpha seed times exp(-f_gap over alpha seed), where alpha seed is defined as 4 pi times 11 and f_gap is the gap weight w8 times ln(phi). This form is introduced as a definition rather than a derived theorem, with the module proving supporting properties such as positivity and the associated logarithmic ODE. Upstream, the definition of alpha inverse in Constants.Alpha directly encodes this product, while alpha seed and f_gap appear in AlphaHigherOrder as the geometric seed from ledger structure and the DFT-8 projection weight respectively.
proof idea
The term proof unfolds the definition of alpha inverse, which expands to alpha seed multiplied by the exponential term, then applies field_simp to cancel the shared alpha seed factor on both sides of the equality.
why it matters
This identity underpins the logarithmic analysis in the same module and is invoked by the downstream theorem log_alphaInv_seed_ratio to obtain the natural log form. It partially addresses the open Gap B noted in the module documentation by verifying the ratio structure of the exponential resummation, though the module explicitly leaves uniqueness of the exponential Taylor coefficients unproved. The result aligns with the Recognition Science derivation of alpha inverse near 137.036 from the phi-ladder and J-cost log-coordinate expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.