module module high

`IndisputableMonolith.Mathematics.ComplexNumbers`

This module defines the eight phases of the recognition tick cycle in complex arithmetic. Recognition Science modelers cite it when handling discrete rotations or periodic states tied to the tick. The module proceeds via targeted definitions of tickPhase and supporting lemmas that establish equivalence to roots of unity while ruling out real-only representations.

claimThe eight phases of the recognition tick cycle are the complex numbers $e^{2 i k /8}$ for integer $k$, satisfying the eighth roots of unity condition with period $2^3$.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and works inside the eight-tick octave structure. It introduces tickPhase as the complex representation of each discrete phase shift, tick_phases_roots_of_unity to equate these phases with roots of unity, and auxiliary results such as reals_no_rotation and phases_require_complex that demonstrate why real scalars alone fail to capture the required rotations.

proof idea

This is a definition module, no proofs. It organizes the argument by first naming the phase objects, then verifying their algebraic closure under multiplication via roots-of-unity identities, and finally exhibiting explicit counterexamples that force the move to complex numbers.

why it matters in Recognition Science

The module supplies the phase infrastructure required by downstream declarations such as quantum_requires_complex, schrodingerEquation, and fourier_uses_complex. It directly implements the T7 eight-tick octave step of the forcing chain, allowing periodic recognition processes to be expressed without additional hypotheses.

scope and limits

Does not treat continuous-time limits or analytic continuation.
Does not derive the Schrödinger equation itself.
Does not supply numerical evaluation routines.
Does not address higher-dimensional or non-periodic extensions.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (21)

def tickPhase L50
theorem tick_phases_roots_of_unity L54
theorem tick_phases_equally_spaced L67
theorem reals_no_rotation L82
theorem complex_rotation L91
theorem phases_require_complex_k1 L104
theorem phases_require_complex_k2 L117
theorem phases_require_complex L128
theorem quantum_requires_complex L164
def schrodingerEquation L171
def phasor L176
theorem fourier_uses_complex L181
theorem complex_inevitable L196
theorem euler_formula L203
theorem quaternions_not_needed L213
theorem split_complex_insufficient L220
theorem complex_is_unique L227
theorem complex_from_ledger L242
def predictions L253
structure ComplexFalsifier L267
def experimentalStatus L274