IsFermionic
plain-language theorem explainer
Defines a ledger state as fermionic when its minimal recognition cycle has period exactly 4. Researchers deriving spin-statistics relations from the eight-tick structure cite this predicate to classify half-integer spin cases. The definition reduces to a direct equality on the input natural number without lemmas or computation.
Claim. A ledger state with recognition period $p$ is fermionic if and only if $p=4$.
background
The SpinStatistics module derives the full spin-statistics theorem from the RS eight-tick ledger. Fermionic states correspond to 4-tick cycles (half the base period), while bosonic states use 1, 2 or 8 ticks. This setup follows the T7 eight-tick octave landmark in the forcing chain.
proof idea
The declaration is a direct definition that assigns the predicate to the equality period = 4. No lemmas are applied and no tactics are used.
why it matters
This supplies the fermionic case for the module's spin_statistics_theorem and pauli_exclusion results. It fills the classification step in the paper RS_Spin_Statistics_Theorem.tex and connects to the eight-tick structure (T7) that forces D=3. The definition closes the basic partition needed for antisymmetry under exchange.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.