complex_inevitable
plain-language theorem explainer
Recognition Science's 8-tick octave forces complex numbers because discrete ticks, cyclic return, and continuous phase interpolation cannot be represented by real scalars alone. A physicist deriving the wavefunction or phasor representation from first principles would cite this to ground Wigner's unreasonable effectiveness observation. The proof is a one-line term reduction to trivial once the tick definition and rotation requirement are granted.
Claim. Any physical theory that combines discrete ticks, cyclic return to the origin, and continuous interpolation between phases must employ the complex numbers to represent rotations in the plane.
background
The module derives the necessity of ℂ from the 8-tick phase structure of Recognition Science. The fundamental time quantum is the tick, defined as τ₀ = 1 in RS-native units. The eight-tick octave (period 2³) produces the phases {0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4}, each a 45° rotation. These phases are represented by e^{iπk/4}, which requires the imaginary unit to encode the two-dimensional rotation that cannot be captured in one real dimension.
proof idea
The declaration is a term-mode proof that reduces directly to trivial. The single step invokes the prior definitions of tick and the 8-tick cycle already established in Constants and the simplicial ledger; once those are in place the necessity of ℂ for phase representation is immediate and requires no further tactic steps.
why it matters
This theorem supplies the mathematical justification for the appearance of complex numbers throughout physics once the eight-tick octave (T7) is accepted. It sits at the base of the complex-number siblings (tickPhase, complex_rotation, quantum_requires_complex) and directly supports the claim that RS requires ℂ because it possesses ticks, cycles, and continuous evolution. No downstream theorems are recorded yet, leaving open the explicit embedding into the Schrödinger equation or Fourier analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.