module module high

`IndisputableMonolith.Constants.AlphaExponentialForm`

This module unfolds the alphaInv formula into an explicit exponential expression using the gap-weight construction. Researchers deriving parameter-free values for the fine-structure constant would cite it when tracing alpha from the 8-tick projection. The module proceeds by successive substitutions that replace the gap term with its closed-form exponential reduction.

claimThe inverse fine-structure constant unfolds as an exponential expression: $f_ {gap} = w_8 · ln(φ)$ is substituted into the alphaInv formula to yield the explicit exponential form without free parameters.

background

The module sits in the constants domain of Recognition Science and imports the RS time quantum τ₀ = 1 tick together with the gap-weight definition. GapWeight supplies the single gap term f_gap = w₈ · ln(φ) as the 8-tick projection weight, required to be parameter-free for the no-free-parameters claim. The Alpha sibling module provides the base alphaInv object that this module then rewrites in exponential form.

proof idea

This is a definition module, no proofs. It organizes the unfolding through a sequence of definitions (alphaInv_def, alphaInv_of_gap) and supporting lemmas that perform the algebraic substitution of the gap term.

why it matters in Recognition Science

The module supplies the exponential reduction step that feeds the numerical verification of alpha^{-1} inside the interval (137.030, 137.039). It closes the gap-weight pipeline in the constants section of the framework, directly supporting the claim that alpha arises from the phi-ladder and eight-tick octave without external parameters.

scope and limits

Does not introduce additional free parameters.
Does not compute explicit numerical values for alphaInv.
Does not treat higher-order radiative corrections.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.GapWeight module_import

declarations in this module (15)

theorem alphaInv_def L57
theorem alpha_seed_positive L60
theorem alphaInv_positive L66
theorem exp_factor_bounded L71
theorem alphaInv_seed_ratio L80
theorem log_alphaInv_seed_ratio L96
theorem log_alphaInv_eq L102
def alphaInv_of_gap L124
theorem alphaInv_of_gap_at_canonical L127
theorem deriv_alphaInv_of_gap L130
theorem logarithmic_derivative_constant L155
theorem alphaInv_linear_term L200
theorem alphaInv_linear_rate L207
def exponential_form_from_constant_log_derivative L242
theorem exponential_form_uniqueness_ode_principle L257