spin_half_from_D3
plain-language theorem explainer
The declaration establishes that spatial dimension D equals 3, which forces the covering group Spin(3) to be isomorphic to SU(2) and thereby permits spin-1/2 representations for fermions. Researchers assembling the Dirac equation in the recognition framework cite this step when certifying the first-order recognition operator for spinors. The proof reduces to a direct reflexivity step once D is fixed by the upstream dimension axiom.
Claim. In the recognition framework the spatial dimension satisfies $D=3$, so that the spin group satisfies Spin(3) ≅ SU(2) and half-integer spin representations exist for fermions.
background
The module derives the Dirac equation (iγ^μ ∂_μ − m)ψ = 0 as the first-order recognition operator equation on the J-cost Hilbert space. The 4-component spinor ψ encodes the recognition state (J, σ, Z, Θ) while the γ matrices realize the Clifford algebra {γ^μ, γ^ν} = 2g^μν coming from the recognition metric. Upstream results supply rung functions that assign integer levels on the phi-ladder to leptons, quarks and bosons; these levels enter the mass formula m_r = φ^r · φ^{-5}.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of D as 3 supplied by the foundational constants.
why it matters
The result supplies the spin_half_from_D3 field required by the DiracEquationCert structure, completing the master certificate that assembles the Dirac equation from J-cost. It realizes the T8 step of the unified forcing chain that forces D = 3 spatial dimensions. The certificate is used downstream to certify both the positivity and monotonicity of the Dirac mass on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.