spinor_dim_D4
plain-language theorem explainer
The equality records that the spinor dimension function returns four when the spatial dimension parameter equals four. A researcher comparing Clifford representations across dimensions or extending the ledger model beyond the forced D=3 case would cite the result. The proof is a direct reflexivity step that evaluates the function definition without further lemmas.
Claim. The spinor representation dimension for spatial dimension four equals four: $spinorDimension(4)=4$.
background
The DimensionForcing module proves spatial dimension D=3 is required by the Recognition Science framework. It combines a topological linking argument (non-trivial knots exist only for D=3) with an eight-tick synchronization condition derived from the 8-tick octave and the 45-tick cumulative phase. The spinorDimension function maps each integer D to the dimension of the minimal spinor representation compatible with the Clifford algebra Cl_D. Upstream, the cost function H is defined by H(x)=J(x)+1, converting the Recognition Composition Law into the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y).
proof idea
The proof is a one-line reflexivity step that directly evaluates the definition of spinorDimension at the input 4.
why it matters
This supplies the D=4 baseline against which the forced D=3 case (spinorDimension(3)=2) is contrasted. It supports the module's characterization that only D=3 produces the two-component, non-abelian, simple spinor structure Spin(3)≅SU(2) needed for gauge interactions. The result sits inside the dimension-forcing chain that begins from Alexander duality and the eight-tick identity 2^D=8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.