pith. sign in
module module high

IndisputableMonolith.Constants.AlphaDerivation

show as:
view Lean formalization →

This module forces D=3 in the alpha derivation by invoking the T9 linking requirement on the Recognition Science geometry. Researchers deriving fundamental constants from the phi-ladder and eight-tick structure cite it to justify three-dimensional space. The module imports the base time quantum and gap-weight definitions, then assembles the D=3 constraint without additional lemmas.

claimThe linking condition T9 requires spatial dimension $D=3$ for the fine-structure derivation pipeline that employs gap weight $w_8$ and the eight-tick projection.

background

The module sits inside the Constants domain and imports the RS-native time quantum $\tau_0=1$ tick together with the gap-weight definition. GapWeight supplies the closed-form projection $f_{\rm gap}=w_8\cdot\ln(\phi)$ used throughout the $\alpha$ pipeline; the weight is required to be parameter-free. The local theoretical setting is the forcing chain that selects D=3 so that isotropic coupling and solid-angle exclusivity can be stated in three dimensions.

proof idea

This is a definition module, no proofs. It consists of three imports that bring the time quantum, the gap weight, and the D=3 constraint into scope for downstream alpha-related derivations.

why it matters in Recognition Science

The module supplies the D=3 premise required by CurvatureSpaceDerivation (integration over five-dimensional configuration space yielding the $\pi^5$ term), SolidAngleExclusivity (isotropic 4$\pi$ factor in D=3), StrongCoupling, HubbleTension, and the mass-anchor derivations. It closes the T9 step that follows T8 in the forcing chain and is cited whenever the alpha band (137.030,137.039) is invoked.

scope and limits

used by (34)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 4 more

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (43)