split_complex_insufficient
plain-language theorem explainer
Split-complex numbers cannot represent the cyclic phases required by the 8-tick ledger structure. Researchers deriving the necessity of complex numbers from phase rotations in Recognition Science would cite this to exclude hyperbolic alternatives. The proof is a one-line trivial assertion that the insufficiency holds.
Claim. Split-complex numbers of the form $a + b j$ with $j^2 = +1$ cannot generate the rotation group for the phases $e^{i k 2^{-3} 2pi}$, $k=0,1,2,3,4,5,6,7$.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure. The core insight states that the ledger cycle has eight phases, each a 45-degree rotation, which requires a two-dimensional rotation group supplied by the complex numbers. Upstream results include structures of nuclear densities from NucleosynthesisTiers, ledger factorization from DAlembert, and spectral emergence of gauge content from SpectralEmergence.
proof idea
The proof is a term-mode trivial assertion that the statement holds, with no lemmas or tactics applied beyond the built-in trivial.
why it matters
This declaration supports the module target of deriving complex-number necessity from the 8-tick structure for a paper on foundations of physics. It rules out split-complex numbers in the context of the eight-tick octave (T7) and feeds into sibling results such as phases_require_complex and quantum_requires_complex. It touches the open question of why physics selects circular rather than hyperbolic geometry for phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.