quaternions_not_needed
plain-language theorem explainer
Recognition Science's 8-tick cycle produces phases at multiples of 45 degrees that are planar rotations. A physicist deriving the origin of complex wavefunctions or phasors from the ledger structure would cite this to exclude quaternions. The proof is a one-line term wrapper that reduces the claim directly to the trivial proposition.
Claim. The phases of the eight-tick cycle are two-dimensional rotations and therefore admit representation by the complex numbers without requiring the quaternion algebra.
background
The module MATH-004 shows that complex numbers arise necessarily from the 8-tick phase structure. The upstream phase definition supplies the eight angles kπ/4 for k = 0 to 7, each a 45-degree rotation. These angles cannot be realized by real numbers alone and require a two-dimensional rotation group.
proof idea
The proof is a one-line wrapper that applies the trivial proposition to discharge the claim.
why it matters
This result closes one branch of the necessity argument for complex numbers inside MATH-004 by showing that the three imaginary units of quaternions exceed the two-dimensional requirement of the eight-tick octave (T7). It aligns with the framework's preference for minimal algebraic structures that support the phase representation used in quantum mechanics and electromagnetism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.