spatial_dims_eq_3
plain-language theorem explainer
The theorem asserts that the spatial dimension count forced by the Recognition Science framework equals three. Researchers deriving the curvature correction δ_κ in the fine-structure constant would cite it when counting the three spatial factors inside the five-dimensional phase-space integral. The proof is a one-line reflexivity that follows immediately from the definition of spatial_dims_forced as the abstract dimension D.
Claim. The spatial dimension forced by the linking requirement of closed curves satisfies $D = 3$.
background
The module shows why the curvature correction in α^{-1} = 4π·11 - f_gap - 103/(102π^5) carries a π^5 denominator: the relevant integral is performed over a five-dimensional configuration space consisting of three spatial dimensions, one temporal phase from the eight-tick cycle, and one dual-balance constraint. The sibling definition spatial_dims_forced simply returns the abstract dimension D supplied by the DimensionForcing module. Upstream results establish that D must be three because linking of closed curves is nontrivial only for D ≥ 3 and vanishes for D > 3.
proof idea
The proof is a direct reflexivity step. It applies the definitional equality spatial_dims_forced = D together with the already-established fact that D equals three.
why it matters
This result supplies the spatial contribution to the five-dimensional configuration space used in the curvature correction. It closes the T8 step of the forcing chain by confirming D = 3, which then combines with the temporal dimension from the eight-tick cycle and the balance dimension to produce the π^5 denominator. The parent derivation appears in the fine-structure constant formula within the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.