split_complex_insufficient
Split-complex numbers with unit j where j squared equals positive one produce hyperbolic geometry and cannot generate the cyclic 8-tick phase rotations required by Recognition Science. A researcher deriving the necessity of complex numbers for quantum phases or Fourier analysis would cite this result to exclude alternative algebras. The proof is a one-line term that reduces the claim directly to the trivial proposition.
claimSplit-complex numbers, defined by adjoining a unit $j$ satisfying $j^2 = +1$, do not admit representations of the cyclic group of order 8 and therefore cannot encode the 45-degree phase steps of the ledger cycle.
background
The module MATH-004 derives the necessity of complex numbers from the 8-tick phase structure: the ledger cycle consists of eight equally spaced phases that correspond to rotations by multiples of 45 degrees. These phases are represented by eighth roots of unity $e^{i k pi / 4}$ for $k = 0$ to 7, which require a two-dimensional rotation algebra. Split-complex numbers replace the imaginary unit with a hyperbolic unit and therefore generate only hyperbolic functions rather than circular ones. Upstream structures such as SpectralEmergence.of establish the discrete phase content of the ledger, while PhiForcingDerived.of supplies the J-cost calibration that fixes the eight-tick octave.
proof idea
The declaration is a term-mode proof that directly supplies the constant trivial for the proposition True. No lemmas are applied; the surrounding doc-comment supplies the geometric distinction between hyperbolic and circular geometry that justifies treating the insufficiency as immediate.
why it matters in Recognition Science
This result closes one branch of the MATH-004 derivation by ruling out split-complex numbers as a substitute for complex phases in the 8-tick structure. It supports the parent claim that the ledger forces the use of complex numbers for quantum mechanics and signal processing. The theorem aligns with framework landmark T7 (eight-tick octave) and the requirement that phases be rotations in the plane.
scope and limits
- Does not prove split-complex numbers are useless in all hyperbolic contexts.
- Does not supply a quantitative comparison of rotation groups.
- Does not address whether split-complex numbers could appear in auxiliary calculations.
- Does not derive the algebraic closure of the complex numbers.
formal statement (Lean)
220theorem split_complex_insufficient :
221 -- Split-complex numbers have hyperbolic, not circular, geometry
222 -- They can't represent cyclic phases
223 True := trivial
proof body
Term-mode proof.
224
225/-- **THEOREM**: ℂ is algebraically closed.
226 This is the Fundamental Theorem of Algebra (proved in Mathlib). -/