Dimension
plain-language theorem explainer
Dimension is defined as the natural numbers in the RS foundation. Researchers deriving that spatial dimension equals 3 from topological linking and eight-tick synchronization would cite this abbreviation to type the variable D. The declaration is a direct abbreviation with no lemmas or computational steps.
Claim. Spatial dimension is represented by a natural number $D$ in the set of natural numbers $D : ℕ$.
background
The Dimension Forcing module proves that spatial dimension D equals 3 is forced by the RS framework. It presents a linking argument: D=1 is collinear with no linking, D=2 unlinks by the Jordan curve theorem, D=3 permits non-trivial knots and links, and D≥4 unlinks by codimension. A second argument requires synchronization of the 8-tick cycle (2^D) with the 45-tick cumulative phase, yielding lcm(8,45)=360 and forcing D=3 via 2^D=8.
proof idea
This is a direct abbreviation. No lemmas are applied and no tactics are used; the declaration simply sets the carrier type for dimension values referenced in downstream results such as spatial_dims_eq_3 and eight_tick_forces_temporal.
why it matters
The abbreviation supplies the type used by spatial_dims_eq_3 (spatial_dims_forced = 3) and eight_tick_forces_temporal (2^D = 8). It occupies the T8 position in the unified forcing chain where D=3 is forced by the eight-tick octave. It also appears in curvature space derivations and pulsar period calculations that depend on the forced dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.