BosonLedgerEntry
plain-language theorem explainer
BosonLedgerEntry packages a complex phase fixed exactly to 1 as the ledger record for integer-spin particles. Researchers deriving spin-statistics from discrete 8-tick cycles would cite the structure when separating boson from fermion entries in the phase ledger. The declaration is a direct structure definition that encodes the even-phase condition without further computation.
Claim. A boson ledger entry consists of a complex phase value together with the constraint that the phase equals 1, corresponding to an even multiple of $2π$ under the 8-tick rotation.
background
The QFT.SpinStatistics module derives the spin-statistics theorem from Recognition Science's 8-tick phase structure. A 2π rotation traverses one full 8-tick cycle; integer spin yields phase +1 after one cycle while half-integer spin yields -1 after two cycles. Upstream, EightTick.phase supplies the discrete phases $kπ/4$ for $k=0..7$, and LedgerFactorization.of calibrates the underlying J-cost on the positive reals.
proof idea
The declaration is a structure definition that directly records the phase field and its equality to 1. No lemmas or tactics are invoked; the body simply asserts the even-phase condition for bosons.
why it matters
The structure supplies the boson half of the phase ledger needed for the spin-statistics derivation in the 8-tick framework. It pairs with the fermion counterpart to enforce symmetric wavefunctions under exchange, fulfilling the module's target of obtaining Bose-Einstein statistics from discrete time. The parent result is the overall spin-statistics theorem stated in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.