measure_dimension
plain-language theorem explainer
The declaration sets the integration measure dimension to five by adding three spatial dimensions to one temporal and one conservation factor. Workers on higher-order voxel-seam corrections to α⁻¹ cite it when forming the π exponent in δ_n terms. The definition is a direct arithmetic assignment with no lemmas or tactics applied.
Claim. The integration measure dimension equals $5$, formed as $D + 1 + 1$ where $D = 3$ is the number of spatial dimensions.
background
The module develops higher-order corrections to the fine-structure constant via the series α⁻¹ = α_seed − f_gap + Σ δ_n. Each δ_n is a combinatorial sum over face-wallpaper pairs on the Q₃ cube, weighted by the Z₂⁵ half-period integration measure. The measure dimension supplies the exponent on π in the denominator of these curvature corrections.
proof idea
One-line definition that directly assigns the natural number 3 + 1 + 1.
why it matters
This supplies the exponent used in delta_1 and the AlphaFrameworkCert structure that certifies readiness for δ₂ computation. It encodes the D = 3 spatial dimensions fixed by T8 of the unified forcing chain, together with the temporal and conservation extensions needed for the half-period measure. The open question it supports is whether the full alternating series converges to the CODATA target 137.035999206(11).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.