Pith. sign in
module module moderate

IndisputableMonolith.Constants.AlphaExponentialForm

show as:
view Lean formalization →

Module that rewrites the RS inverse fine-structure constant as an explicit exponential in the gap weight and φ. Anyone deriving α^{-1} in the (137.030, 137.039) band, or differentiating it in the gap parameter, cites these identities. The development is algebraic: seed ratio, log form, gap-parameterized family, and a constant logarithmic derivative.

claimThe RS inverse fine-structure constant $\alpha^{-1}$ is written in exponential form $\alpha^{-1} = S\, e^{c\, f_{\mathrm{gap}}}$ (equivalently via a seed ratio and $\log\alpha^{-1}$), where $f_{\mathrm{gap}} = w_8\ln\varphi$ is the single 8-tick gap term and $S$ is the positive seed. The module also treats $\alpha^{-1}$ as a smooth function of the gap, records its derivative, and isolates the linear term in that expansion.

background

Recognition Science fixes dimensionless constants from the forcing chain and the Recognition Composition Law, with $\varphi$ the self-similar fixed point (T6) and the eight-tick octave (T7) supplying the discrete period behind gap weights. In RS-native units the fine-structure target is the narrow band $\alpha^{-1}\in(137.030,137.039)$.

The Alpha and GapWeight imports supply the raw $\alpha^{-1}$ construction and the parameter-free weight $w_8$. GapWeight states that the $\alpha$ pipeline uses a single gap term $f_{\mathrm{gap}}=w_8\cdot\ln\varphi$, and that $w_8$ must be a closed form rather than a numeric certificate if the no-free-parameters claim is to hold. Constants supplies the ambient RS units (including the time quantum $\tau_0$).

This module sits between those definitions and any later numerical or analytic use of $\alpha^{-1}$: it unfolds the inverse-alpha formula into exponential, logarithmic, and gap-parameterized shapes needed for positivity, bounds, and differentiation.

proof idea

Definition-first module with a short chain of supporting lemmas, not a single deep proof. It introduces the exponential unfolding of $\alpha^{-1}$, proves the seed and $\alpha^{-1}$ are positive, and bounds the exponential factor. Ratio and log identities relate $\alpha^{-1}$ to the seed; a gap-parameterized form $\alpha^{-1}(f)$ is defined and evaluated at the canonical gap. Differentiation yields a constant logarithmic derivative and isolates the linear term in the gap expansion. Arguments are standard real-analytic manipulations over the imported closed forms for $\varphi$ and $w_8$.

why it matters in Recognition Science

Without an exponential/gap form, $\alpha^{-1}$ remains a opaque constant definition and cannot be differentiated or matched to the RS alpha band under variation of $w_8$. The module makes the single-gap structure $f_{\mathrm{gap}}=w_8\ln\varphi$ operational: positivity and seed-ratio lemmas underwrite well-definedness; the gap family and constant logarithmic derivative support sensitivity and linear-response arguments around the canonical eight-tick weight.

Downstream edges are not yet wired in the graph (used_by empty), but the natural consumers are any theorem that quotes the RS $\alpha^{-1}$ band, compares seed versus full inverse alpha, or expands $\alpha^{-1}$ to first order in the gap. That sits on the constants side of the same forcing story that produces $\varphi$, the eight-tick octave, and $D=3$. Historically $w_8$ was a numeric certificate; pairing GapWeight's closed form with this exponential unfolding is part of closing the no-free-parameters claim for $\alpha$.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (15)