D4_no_spinor_structure
plain-language theorem explainer
Four spatial dimensions fail the RS spinor structure because Spin(4) factors as SU(2)×SU(2) and therefore violates the simplicity clause. Researchers deriving spatial dimension from Clifford algebra properties in Recognition Science would cite this to exclude D=4 from the allowed set. The proof assumes the structure for D=4 and obtains an immediate contradiction by case analysis on the simplicity disjunct followed by numerical normalization.
Claim. Dimension four does not satisfy the RS spinor structure conditions: it fails to have two-component spinors in the required sense (spinor dimension equals 2 or the dimension equals 3), Spin(4) is not simple (dimension equals 3 or dimension at least 5), even though the non-abelian condition holds.
background
The DimensionForcing module proves that spatial dimension D=3 is forced by the RS framework. One argument replaces the topological linking axiom with a Clifford-algebra characterization: a dimension has the required spinor structure when spinors are two-component, Spin(D) is non-abelian, and Spin(D) is simple. The structure HasRSSpinorStructure encodes exactly these three requirements, noting that only D=3 yields Cl₃ ≅ M₂(ℂ) and Spin(3) ≅ SU(2). Upstream constants supply the fundamental tick τ₀ = 1 that underlies the eight-tick octave used elsewhere in the module.
proof idea
The term proof assumes HasRSSpinorStructure 4, which supplies the simplicity clause (D=3 or D≥5). Case analysis on that disjunction produces either the equation 4=3 or the inequality 4≥5; both are discharged by norm_num.
why it matters
The declaration closes one route to D=4 inside the dimension-forcing argument that replaces the linking axiom with a spinor-structure characterization. It directly supports the claim that only D=3 satisfies both the eight-tick condition (2^D) and the simplicity requirement on Spin(D), consistent with T7 and T8 of the forcing chain. No downstream theorems depend on it yet; it functions as a negative filter within the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.