IndisputableMonolith.Constants.AlphaExponentialForm
AlphaExponentialForm module unfolds the alphaInv formula to its explicit exponential expression in the Recognition Science constants pipeline. Researchers deriving fundamental constants from the gap-weighted alpha formula would cite it for the closed form. The module consists of sequential definitions and equalities that reduce the formula using imported gap and alpha components.
claim$\alpha^{-1}$ unfolds to the exponential expression $\exp(f_{\rm gap} + \dots)$ with $f_{\rm gap} = w_8 \ln\phi$.
background
The module sits in the constants domain and imports the RS time quantum $\tau_0 = 1$ tick. It draws on the Alpha module for base definitions and on GapWeight, which states: "In the $\alpha$ pipeline we use a single gap term: $f_{\rm gap} = w_8 \cdot \ln(\phi)$." The same upstream note requires $w_8$ to be parameter-free to uphold the no-free-parameters claim.
Sibling declarations in the module (alphaInv_def, alphaInv_of_gap, log_alphaInv_eq) supply the concrete objects that the exponential unfolding acts upon.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supports the alpha constants pipeline that targets the band $(137.030, 137.039)$. It supplies the exponential form required by the module doc-comment and feeds downstream constant derivations even though no explicit used_by edges are recorded.
scope and limits
- Does not derive a numerical value for $\alpha^{-1}$.
- Does not introduce free parameters beyond the imported gap weight.
- Does not treat other constants such as $G$ or $\hbar$.
- Does not address spatial dimension or forcing-chain steps T0-T8.
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