fermi_exchange_sign
plain-language theorem explainer
The half-cycle eight-tick phase equals −1, the fermionic exchange sign. Cosmology and statistical-mechanics arguments cite it as the sole RS input that forces Pauli occupancy {0,1} in the Fermi single-mode partition. The proof is a one-line projection of the spin-statistics key theorem.
Claim. The complex phase factor at eight-tick index $k=4$ (half-cycle) equals $-1$: $\mathrm{phaseExp}(4)=-1$.
background
The module builds per-mode grand partition functions for cosmology thermal history. Bose modes sum over all $\mathbb{N}$ occupancies; Fermi modes are restricted to ${0,1}$. With $x=e^{-t}$ and $t>0$, both series converge, giving $Z_B=(1-x)^{-1}$ and $Z_F=1+x$, hence the log kernels and mean occupations $1/(e^t\mp 1)$.
The only physical fork is that occupancy range. In Recognition Science it comes from the eight-tick octave (forcing chain T7): discrete phases on $\mathrm{Fin},8$, with $\mathrm{phaseExp}(k)=\exp(i,\mathrm{phase}(k))$. The spin-statistics key theorem states that the half-cycle phase ($k=4$) is $-1$ and the identity phase ($k=0$) is $+1$, linking the eight-tick structure to fermion antisymmetry versus boson symmetry.
Standard antisymmetrization then forces double occupancy to vanish, so the Fermi sum is indexed by $\mathrm{Fin},2$. That step is a choice of statement, not a hidden axiom; everything after the fork is pure analysis.
proof idea
One-line term proof: project the left conjunct of spin_statistics_key, which already proves $\mathrm{phaseExp}\langle 4\rangle=-1\land\mathrm{phaseExp}\langle 0\rangle=1$ via the elementary evaluations phase_4_is_minus_one and phase_0_is_one. No extra algebra is done here.
why it matters
This re-export is the honest RS input for the Fermi side of PartitionKernels. Module documentation scopes it as the sole physical fact that justifies Pauli restriction before deriving $Z_F=1+x$ and $\mathrm{fermiLogKernel}$. Downstream, the sibling partition and log-kernel theorems (and the pressure/entropy integrals in PhaseSpaceReduction) rest on that fork; the listed use edge into the Bose log-kernel identity sits in the same certified block.
Framework landmark: eight-tick octave (T7) and the spin-statistics bridge from Foundation.EightTick. Without half-cycle phase $-1$, the Bose/Fermi split would be an external postulate rather than an RS-derived occupancy choice. The step from exchange sign to occupancy $\le 1$ remains the classical antisymmetrization argument, used openly as justification for the index type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.