spatial_dims_forced
plain-language theorem explainer
The declaration defines spatial_dims_forced as the natural number D. Researchers deriving the curvature correction term in the fine structure constant would cite this when isolating the spatial contribution to the five-dimensional configuration space. It is a direct definition that aliases the dimension count fixed by the closed-curve linking requirement.
Claim. Define the spatial dimension count as the natural number $D$, the unique value making linking of closed curves non-trivial.
background
The module shows that the curvature correction integrates over a five-dimensional configuration space whose factors are three spatial dimensions, one temporal dimension from the eight-tick cycle, and one balance dimension from the conservation constraint; each angular integration contributes a factor of π, producing the π^5 in the denominator of δ_κ. This declaration supplies the spatial component of that total. The module documentation states that in D dimensions linking of closed curves is only non-trivial when D ≥ 3, while for D > 3 the link penalty vanishes, so D = 3 is the unique stable dimension.
proof idea
One-line definition that directly sets spatial_dims_forced equal to the constant D imported from the Constants module.
why it matters
This definition supplies the spatial factor to the theorem config_space_complete, which sums the three forced dimensions to obtain the total five-dimensional space responsible for π^5 in the curvature term of the alpha derivation. It implements the spatial part of the T8 step in the forcing chain. The downstream theorem spatial_dims_eq_3 then specializes the definition to the concrete value 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.