why_D_equals_3
plain-language theorem explainer
The theorem shows that spatial dimension equals three because spinor structure plus the eight-tick condition together force D=3, the RS-compatible dimension is unique, and the physical dimension is fixed at three. A physicist deriving spacetime from ledger topology or Clifford algebra would cite this when replacing the postulate D=3 with a forcing argument. The proof is a single term that packages four sub-lemmas: spinor forcing, eight-tick forcing, uniqueness of compatible dimension, and reflexivity on the physical value.
Claim. For every dimension $D$, if $D$ admits the RS spinor structure (two-component spinors, non-abelian simple Spin group) and the eight-tick cycle equals 8, then $D=3$; likewise, the eight-tick condition alone forces $D=3$. There exists a unique RS-compatible dimension (non-trivial linking, eight-tick synchronization, gap-45 compatibility). The physical spatial dimension equals 3.
background
The module proves spatial dimension is forced rather than chosen. HasRSSpinorStructure requires two-component spinors, non-abelian Spin(D), and simplicity; it characterizes D=3 via Cl_3 ≅ M_2(ℂ) and Spin(3) ≅ SU(2). EightTickFromDimension is the definition 2^D. RSCompatibleDimension collects three conditions: SupportsNontrivialLinking, EightTickFromDimension D = 8, and 2^D divides the synchronization period. D_physical is the constant 3. The local setting is the four-argument forcing chain: topological linking via Alexander duality is primary, while spinor, Bott, and gap-45 arguments are consequences. Upstream, alexander_duality_circle_linking states SphereAdmitsCircleLinking D ↔ D=3, proved from reduced cohomology of S^1 by the relation H̃^{D-2}(S^1) nontrivial iff D-2=1.
proof idea
The proof is the term ⟨spinor_eight_tick_forces_D3, eight_tick_forces_D3, dimension_forced, rfl⟩. It directly assembles the four conjuncts of the statement. spinor_eight_tick_forces_D3 and eight_tick_forces_D3 are in-module lemmas that apply the spinor structure and the definition EightTickFromDimension D = 2^D. dimension_forced is the sibling theorem that extracts uniqueness of RSCompatibleDimension from the linking predicate. rfl discharges the final equality D_physical = 3 by definition.
why it matters
This is the terminal theorem of the DimensionForcing module and the explicit statement of T8 in the forcing chain. It resolves the T7/T8 circularity by deriving the eight-tick octave as a consequence of D=3 via Alexander duality alone, rather than assuming periodicity first. The result feeds the ledger synchronization arguments and the gap-45 construction that produce the 360-degree period. It closes the question of why the universe has three spatial dimensions by exhibiting a cohomological obstruction that exists only for D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.