pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.AlphaDerivation

show as:
view Lean formalization →

The AlphaDerivation module forces the spatial dimension D to equal 3 via T9 linking constraints on cube geometry, closing the parameter-free pipeline for the fine structure constant. Researchers deriving fundamental constants from the J-functional equation would cite it to anchor isotropic coupling in three dimensions. The module assembles definitions for cube vertices, edges, faces, and gap weights to enforce the eight-tick octave structure without free parameters.

claimThe spatial dimension satisfies $D=3$ when the T9 linking condition requires that connections close only inside the eight-tick octave, yielding the inverse fine structure constant band $137.030 < 1/α < 137.039$.

background

Recognition Science begins with the J-cost functional equation whose self-similar fixed point is phi. The upstream Constants module supplies the time quantum τ₀ = 1 tick. GapWeight supplies the closed-form 8-tick projection weight w₈, entering the alpha pipeline through the single gap term f_gap = w₈ · ln(φ). This module introduces the D=3 cube geometry: cube_vertices, cube_edges, cube_faces, vertices_at_D3, edges_at_D3, faces_at_D3, active_edges_per_tick, passive_field_edges, passive_edges_at_D3, cube_dihedral, and faces_per_vertex.

proof idea

This module is a definition module, no proofs. It enumerates the combinatorial structure of the unit cube in three dimensions, defines D explicitly as three, and derives the counts of active and passive edges per tick together with the dihedral angles that enforce isotropy. The argument closes by showing that linking is possible only when the spatial dimension equals three.

why it matters in Recognition Science

The module supplies the D=3 foundation required by downstream derivations including CurvatureSpaceDerivation (why the curvature correction involves π⁵), SolidAngleExclusivity (why the geometric seed is 4π), StrongCoupling (alpha_s from phi-geometry), HubbleTension, and the mass anchor derivations. It fills the T9 step in the forcing chain where linking requires D=3, anchoring the alpha band inside (137.030, 137.039) and the eight-tick octave.

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)