Foundation Dimension Forcing D1 No Spinor Structure

The one-dimensional case

In physics, a spinor is a mathematical object that describes the intrinsic angular momentum of particles like electrons. In three dimensions, these objects have two complex components, which is why we speak of spin-1/2 particles. The Recognition Science framework asks a sharper question: in which spatial dimensions can such a two-component complex spinor structure exist at all? Its machine-checked library of formal theorems contains a declaration, D1_no_spinor_structure, that answers this question for the simplest case.

The declaration proves that in one spatial dimension, the framework's condition for having a spinor structure fails. The condition, called recognition (the framework's term for a discrete record of events), requires a two-component spinor and a non-abelian rotation group, meaning rotations do not commute. In one dimension, there is only a single line, so there are no rotations to speak of, and the framework's arithmetic confirms that the required structure is absent. The theorem is a formal proof, checked by the machine, that the property HasRSSpinorStructure 1 is false.

This is a negative result, but it is load-bearing. The framework proves that only in three dimensions does the spinor structure exist with the required properties. One dimension cannot host it, two dimensions cannot host it, and four dimensions cannot host it. The declaration for one dimension is one of the boundary cases that makes the three-dimensional result sharp. It is the framework's way of saying that the familiar two-component spinor of particle physics is not a generic possibility; it is a special feature of three-dimensional space.

The declaration does not claim that one-dimensional physics is impossible, nor that spinors cannot be defined in one dimension by some other means. It claims only that the specific structure the framework requires, a two-component complex spinor with a non-abelian rotation group, does not exist there. The proof is a theorem about the framework's own definitions, not a statement about the physical world outside that framework. The framework's library shows that the same absence holds for dimensions two and four, and that only dimension three satisfies the full condition.

/-- D = 1 does not have RS spinor structure (too few dimensions). -/
theorem D1_no_spinor_structure : ¬HasRSSpinorStructure 1 := by
  intro ⟨_, hna, _⟩
  norm_num at hna

/-- D = 1 does not have RS spinor structure (too few dimensions). -/
theorem D1_no_spinor_structure : ¬HasRSSpinorStructure 1 := by
  intro ⟨_, hna, _⟩
  norm_num at hna

/-- D = 3 has the RS spinor structure. -/
theorem D3_has_spinor_structure : HasRSSpinorStructure 3 := {
  two_component := Or.inr rfl
  nonabelian := le_refl 3
  simple := Or.inl rfl
}

/-- D = 1 does not have RS spinor structure (too few dimensions). -/
theorem D1_no_spinor_structure : ¬HasRSSpinorStructure 1 := by
  intro ⟨_, hna, _⟩
  norm_num at hna

What this page does not claim

The declaration does not prove that spinors are impossible in one dimension by any definition. The declaration does not claim that one-dimensional physics is inconsistent or impossible. The declaration does not establish that the framework's spinor condition is the only valid way to define spinors.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DimensionForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: