alphaInv_positive
plain-language theorem explainer
Positivity of the inverse fine-structure constant follows from its definition as the product of a positive seed and a positive exponential factor. Researchers deriving constants from Recognition Science structure would cite this to confirm the exponential resummation satisfies the physical requirement of positivity. The proof is a term-mode one-liner that unfolds the definition and applies mul_pos to the seed positivity theorem together with Real.exp_pos.
Claim. The inverse fine-structure constant defined by $0 < alphaInv$ where $alphaInv = alpha_seed * exp(-f_gap / alpha_seed)$, with $alpha_seed = 4 pi * 11$ and $f_gap = w_8 ln phi$, satisfies $0 < alphaInv$.
background
The module analyzes structural properties of the exponential form for the inverse fine-structure constant. In Constants/Alpha.lean the canonical definition is $alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed))$, where $alpha_seed = 4 pi * 11$ is forced by prior derivation and $f_gap = w_8 ln phi$ arises from the eight-tick gap weight. This theorem confirms the expression yields a positive value, as required for physical consistency and noted in the module documentation as the first structural property proved here.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of alphaInv and invokes mul_pos on the upstream theorem alpha_seed_positive together with Real.exp_pos applied to the negative gap term. No additional tactics are required.
why it matters
This result is invoked directly by the downstream log_alphaInv_eq to justify the logarithm of a positive quantity and by the open exponential_form_uniqueness_ode_principle. It fills the positivity step in the module's structural analysis of the exponential form, which is motivated by J-cost log-structure and treated as a bridge claim in the Recognition Science derivation of constants. The module leaves uniqueness of the exponential form among possible resummations as an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.