Pith. sign in
module module moderate

IndisputableMonolith.Constants.AlphaPrecision

show as:
view Lean formalization →

Module packaging the RS fine-structure seed, curvature and gap corrections, and a precision certificate that places α^{-1} in a tight numerical window. Constant-matchers and anyone wiring RS units to CODATA cite the seed bounds and the certificate. Content is definitions plus elementary positivity and interval lemmas.

claimDefines an RS seed $\alpha_{\mathrm{seed}}$, positive curvature and gap corrections, and a certificate that the corrected inverse fine-structure value lies in a narrow interval compatible with the RS band $(137.030,137.039)$.

background

Recognition Science fixes the inverse fine-structure constant inside the window $(137.030,137.039)$ once $c$, $\hbar=\varphi^{-5}$ and $G=\varphi^5/\pi$ are set in RS-native units. The parent Constants module supplies the fundamental time quantum $\tau_0=1$ tick and the $\varphi$-ladder infrastructure.

This module isolates a concrete seed value for $\alpha$ together with two named positive corrections (curvature and gap). Sibling facts record positivity and crude bounds such as $132<\alpha_{\mathrm{seed}}<176$, which the precision certificate later tightens.

proof idea

Definition-and-bounds module, not a forcing argument. It introduces the seed, the two correction terms, and an existence certificate AlphaPrecisionCert. Supporting lemmas are direct positivity checks and elementary interval comparisons; no multi-step derivation from J-uniqueness or the eight-tick octave lives here.

why it matters in Recognition Science

Anchors the numerical value of $\alpha$ inside the RS constants layer. Any later matching of RS units to experiment, or any derivation that closes the alpha band from the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick) or the Recognition Composition Law, imports these definitions. Used_by is presently empty; the module is infrastructure for the constants domain rather than a leaf in a finished theorem.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)