electron_is_fermion
plain-language theorem explainer
The declaration confirms that the electron spin value of 1/2 satisfies the half-integer predicate in the Recognition Science spin structure, establishing its fermionic character under the spin-statistics link. Researchers deriving Pauli exclusion from ledger single-occupancy would cite this when connecting half-integer spin to antisymmetric wavefunctions and single-state occupancy. The proof applies a decision procedure directly to the integer arithmetic of the spin definition.
Claim. The spin value $s = 1/2$ satisfies the half-integer condition $2s$ odd, i.e., $2s % 2 = 1$.
background
The Spin structure encodes quantum spin as twice the value in integers with a non-negativity guard. The half definition sets this twice-value to 1, corresponding to electron (and quark) spin. The isHalfInteger predicate checks whether twice the spin is odd, marking fermions whose wavefunctions pick up a minus sign under exchange. The module derives Pauli exclusion from ledger single-occupancy: fermions carry an odd phase through the eight-tick cycle, so two identical entries at the same address would force the wavefunction to vanish. Upstream, PrimitiveDistinction supplies the seven-axiom foundation that yields the structural conditions used here, while the SpinStatistics module defines the half and isHalfInteger objects.
proof idea
One-line wrapper that applies the decide tactic to the arithmetic predicate on the spin structure.
why it matters
This supplies the fermionic classification for electrons inside the QFT module, feeding the ledger-based derivation of Pauli exclusion and atomic shell structure. It directly implements the odd-phase property for half-integer spins in the eight-tick octave, linking to the paper target of first-principles periodic table and degeneracy pressure. No downstream uses are recorded yet, leaving open how the result composes with explicit rung-fraction embeddings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.