IndisputableMonolith.Constants.AlphaExponentialForm
This module shows that the alphaInv formula in Recognition Science unfolds into an explicit exponential expression. Researchers deriving the fine-structure constant from the phi-ladder and gap weights cite it to confirm the form stays parameter-free. The module is a pure definition and import structure with no internal proofs.
claim$\alpha^{-1}$ unfolds to an exponential expression built from the gap weight $w_8 \cdot \ln(\phi)$ and the RS time quantum $\tau_0 = 1$ tick.
background
The module resides in the Constants domain and imports the base Constants module (defining $\tau_0 = 1$ tick), the Alpha module, and GapWeight. GapWeight supplies the single gap term $f_{\rm gap} = w_8 \cdot \ln(\phi)$ required for the $\alpha$ pipeline; the weight is required to be a closed-form, parameter-free object. The local setting is the derivation of constants from the forcing chain (T5 J-uniqueness through T8 $D=3$), with $\alpha^{-1}$ required to lie inside the interval (137.030, 137.039).
proof idea
This is a definition module, no proofs. It organizes the exponential unfolding of alphaInv by importing the gap-weight definition and the base constants, then exposing the resulting expression through sibling declarations such as alphaInv_of_gap.
why it matters in Recognition Science
The module supplies the exponential form needed downstream in the alpha pipeline. It supports the claim that $\alpha^{-1}$ emerges without free parameters once the gap weight and phi-ladder are fixed, feeding the overall constant-derivation chain that begins from the Recognition Composition Law and the eight-tick octave.
scope and limits
- Does not compute a numerical value for alphaInv.
- Does not introduce additional free parameters.
- Does not prove bounds or convergence of the exponential form.
- Does not address higher-order corrections beyond the gap term.
depends on (3)
declarations in this module (15)
-
theorem
alphaInv_def -
theorem
alpha_seed_positive -
theorem
alphaInv_positive -
theorem
exp_factor_bounded -
theorem
alphaInv_seed_ratio -
theorem
log_alphaInv_seed_ratio -
theorem
log_alphaInv_eq -
def
alphaInv_of_gap -
theorem
alphaInv_of_gap_at_canonical -
theorem
deriv_alphaInv_of_gap -
theorem
logarithmic_derivative_constant -
theorem
alphaInv_linear_term -
theorem
alphaInv_linear_rate -
def
exponential_form_from_constant_log_derivative -
theorem
exponential_form_uniqueness_ode_principle