pith. sign in
module module high

IndisputableMonolith.Constants.AlphaDerivation

show as:
view Lean formalization →

AlphaDerivation module supplies the D=3 geometry and gap-weight pipeline that feeds the fine-structure-constant derivation in Recognition Science. Researchers deriving constants from the forcing chain cite it for the T9 link between linking topology and spatial dimension. The module consists of definitions for cube combinatorics and the 8-tick projection weight w₈ applied to ln(φ).

claimThe module defines the spatial dimension $D=3$ forced by T9 together with the gap term $f_ {gap}=w_8·ln(φ)$ and the associated cube primitives (vertices, edges, faces) required for the isotropic-coupling factor $4π$ in the α pipeline.

background

Constants supplies the base time quantum τ₀=1 tick. GapWeight supplies the single gap term used throughout the α pipeline: f_gap=w₈·ln(φ), where w₈ is the parameter-free 8-tick projection weight. The module therefore sits at the intersection of the Recognition Composition Law and the T8–T9 forcing steps that fix D=3.

proof idea

This is a definition module, no proofs. It enumerates the cube primitives (vertices_at_D3, edges_at_D3, faces_at_D3, active_edges_per_tick, passive_edges_at_D3) and the dihedral and vertex-face relations needed to close the isotropic-coupling argument.

why it matters in Recognition Science

The module supplies the D=3 geometry required by downstream derivations: CurvatureSpaceDerivation (δ_κ involving π^5), SolidAngleExclusivity (4π forced by isotropic coupling), StrongCoupling, HubbleTension, and the mass-anchor chain. It closes the T9 step that links topology to three spatial dimensions.

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)