spinor_eight_tick_forces_D3
plain-language theorem explainer
Any dimension D that carries the RS spinor structure and satisfies the eight-tick period must equal 3. Researchers deriving spacetime dimension from algebraic or Clifford constraints cite the result to close the forcing chain. The argument is a direct one-line application of the eight-tick forcing lemma once the spinor hypotheses are given.
Claim. Let $D$ be a natural number. If $D$ admits two-component spinors whose spin group is non-abelian and simple, and if the period $2^D$ equals the fundamental eight-tick cycle, then $D=3$.
background
The DimensionForcing module proves spatial dimension equals 3 by combining topological linking with algebraic synchronization. Dimension is formalized as a natural number. EightTickFromDimension D is defined as $2^D$, the octave period required by the RS framework. HasRSSpinorStructure D is the proposition that spinors are two-component, Spin(D) is non-abelian, and Spin(D) is simple; for D=3 this recovers Spin(3) ≅ SU(2) and Cl_3 ≅ M_2(ℂ).
proof idea
The proof is a one-line wrapper that applies the eight_tick_forces_D3 lemma to the supplied dimension D and the eight-tick equality hypothesis.
why it matters
The declaration supplies one conjunct inside the parent theorem why_D_equals_3 that assembles all routes to D=3. It realizes the T8 step of the unified forcing chain by replacing the Alexander-duality linking axiom with a Clifford-algebra characterization. The module documentation notes that the eight-tick synchronization with the 45-tick phase further isolates D=3 via lcm(8,45)=360. An open question is whether the full spinor axioms follow from the Recognition Composition Law without extra structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.