spinor_dim_D4
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the forcing of D=3 from spinor properties.
- Does not invoke the topological linking or gap-45 arguments.
- Does not compute spinorDimension for any D other than 4.
- Does not connect to the Recognition Composition Law or cost algebra.
formal statement (Lean)
201theorem spinor_dim_D4 : spinorDimension 4 = 4 := rfl
proof body
Term-mode proof.
202
203/-- A dimension has the RS-required spinor structure if:
204 1. Spinors are 2-component (spin-½ particles)
205 2. Spin(D) is non-abelian (for gauge interactions)
206 3. Spin(D) is simple (not a product)
207
208 **Scope note**: This structure describes D=3 as having the right Clifford/spinor
209 properties (Cl₃ ≅ M₂(ℂ), Spin(3) ≅ SU(2)). It is a *characterization* of why
210 D=3 is physically special, not the derivation. The formal proof that D=3 is
211 forced rests on Alexander duality: the linking group H̃^{D-2}(S¹) = ℤ iff D = 3.
212 The spinor conditions (two_component, nonabelian, simple) and the 8-tick identity
213 (2^D = 8) are derived as *consequences* of D=3, not used as premises. -/