Pith. sign in
module module moderate

IndisputableMonolith.Constants.AlphaDerivation

show as:
view Lean formalization →

The module forces the spatial dimension to D=3 via the linking requirement of T9 in the Recognition Science chain. Researchers deriving the fine structure constant and related constants cite it to justify three-dimensional geometry in the alpha pipeline. It supplies the supporting combinatorial definitions that encode the D=3 constraint without free parameters.

claimThe spatial dimension satisfies $D=3$, as required by the linking condition in T9 of the forcing chain.

background

The module sits in the Constants domain and imports the RS time quantum $ au_0=1$ tick together with the gap weight $w_8$ defined so that $f_{ m gap}=w_8 m ln(\phi)$. Its local setting is the alpha derivation pipeline that begins from the recognition composition law and the eight-tick octave. Sibling definitions supply the cube combinatorics (vertices, edges, faces) that realize the three-dimensional geometry forced by T9.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the D=3 foundation required by downstream modules including CurvatureSpaceDerivation (which isolates the $ m au^5$ curvature term), SolidAngleExclusivity (which forces the $4 m au$ isotropic factor), StrongCoupling, and the mass anchor derivations. It completes the T9 step that links the recognition graph to three spatial dimensions and thereby anchors the parameter-free alpha band (137.030, 137.039).

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)