FermionLedgerEntry
plain-language theorem explainer
FermionLedgerEntry defines a ledger record for fermions as a complex phase fixed to exactly -1, capturing odd phase accumulation under the 8-tick cycle. Researchers deriving spin-statistics from discrete time structures cite this when building antisymmetric wavefunctions from phase rules. The definition is a structure with a single equality constraint on the phase field.
Claim. A fermion ledger entry is a pair consisting of a complex phase $phi in mathbb{C}$ together with the assertion that $phi = -1$.
background
Recognition Science derives spin-statistics from phase accumulation across the 8-tick cycle, where a 2pi rotation traverses one full period. The fundamental time quantum is the tick, defined as tau_0 = 1. Upstream results supply the discrete phases k pi / 4 for k in Fin 8 from the EightTick module and the tick constant from Constants. The module sets the local setting as a derivation of Fermi-Dirac versus Bose-Einstein statistics from whether the accumulated phase under exchange is -1 or +1.
proof idea
This declaration is a structure definition with no proof body. It introduces the type via two fields: the phase component and the explicit equality constraint phase = -1.
why it matters
The structure supplies the fermion half of the ledger model that supports derivation of antisymmetric wavefunctions from odd phase in the 8-tick octave. It implements the phase mechanism for half-integer spin stated in the module documentation and prepares the ground for the boson symmetry claim labeled QFT-003. The entry connects directly to the T7 eight-tick octave landmark in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.