numDiscretePhases
plain-language theorem explainer
The definition fixes the number of discrete phases in a full rotation at the integer 8. Researchers modeling quantum anomalies via 8-tick phase quantization in Recognition Science cite this constant when counting steps in the discrete cycle. It is introduced by direct assignment with no computation or lemmas.
Claim. The number of discrete phases in one full rotation is defined to be $8$.
background
The QFT.Anomalies module derives anomalies from mismatches between continuous phase symmetry and the discrete 8-tick cycle. Phase is introduced upstream as the finite type Fin 8 in both ChurchTuringPhysicsStructure and EightTick, representing the eight labeled states 0 through 7 in one cycle. This definition supplies the cardinality of that phase space for use in anomaly calculations.
proof idea
Direct definition that assigns the constant 8. No tactics or lemmas are invoked; the value is hard-coded to match the 8-tick structure established in the upstream Phase abbrevs.
why it matters
This constant is the immediate input to the eight_quanta_full_rotation theorem, which shows that eight phase quanta close a full 2π rotation and thereby quantifies the phase mismatch that produces anomalies. It instantiates the eight-tick octave (T7) from the Recognition Science forcing chain, where the period is fixed at 2^3. The module doc-comment frames the result as the discrete-time origin of the chiral anomaly for processes such as π⁰ decay.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.