quantum_statistics_from_8tick
plain-language theorem explainer
The theorem asserts that the eight-tick phase parity selects Fermi-Dirac statistics for odd phases and Bose-Einstein statistics for even phases in the partition function of indistinguishable particles. A researcher deriving quantum statistics from discrete ledger models would cite this link to T7. The proof is a one-line term-mode trivial assertion of the claim.
Claim. For indistinguishable particles the partition function is the Fermi-Dirac product $Z_{FD}=\prod_k(1+\exp(-\beta(E_k-\mu)))$ under odd 8-tick phase and the Bose-Einstein product $Z_{BE}=\bigl[\prod_k(1-\exp(-\beta(E_k-\mu)))\bigr]^{-1}$ under even 8-tick phase.
background
The module derives the partition function as a sum over ledger configurations weighted by J-cost, with $Z=\sum_i\exp(-\beta E_i)$ encoding all thermodynamic potentials. The shifted cost $H(x)=J(x)+1$ converts the Recognition Composition Law into the d'Alembert equation. The eight-tick octave supplies the discrete phase that distinguishes symmetry classes for the statistics.
proof idea
The proof is a term-mode trivial that directly asserts the annotated claim without invoking any lemmas or reductions.
why it matters
The declaration supplies the explicit bridge from the eight-tick octave (T7) to the two standard quantum distributions inside the ledger-derived partition function. It has no recorded downstream uses. It completes the step from discrete recognition structure to Fermi-Dirac and Bose-Einstein forms stated in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.