module module high

`IndisputableMonolith.Mathematics.ComplexNumbers`

Mathematics.ComplexNumbers supplies the complex-number infrastructure for the eight phases of the recognition tick cycle. Researchers modeling the eight-tick octave cite it when phase rotations or roots of unity appear. The module proceeds through successive definitions and lemmas that first introduce tickPhase, then demonstrate the necessity of complex structure over the reals.

claimThe eight phases of the tick cycle are the eighth roots of unity in $\mathbb{C}$, represented by the map tickPhase that assigns to each phase index $k$ the value $\exp(2\pi i k/8)$.

background

The module imports Mathlib for complex arithmetic and IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum: "The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick."

It therefore works in the setting where time is discrete in ticks and the cycle length is fixed at eight ticks. The sibling declarations introduce tickPhase, show that the phases are roots of unity and equally spaced, prove that the reals admit no nontrivial rotation, and establish that complex numbers are required for phases, quantum mechanics, and Fourier transforms.

proof idea

This is a definition module, no proofs. It consists of a chain of definitions (tickPhase, phasor) followed by lemmas that successively rule out real-only models and affirm the complex representation needed for the eight-phase cycle.

why it matters in Recognition Science

The module supplies the phase machinery required by the eight-tick octave (T7) in the forcing chain. It directly supports the sibling results on quantum mechanics and Fourier analysis that appear later in the same file; those results in turn feed higher-level statements about the recognition cycle.

scope and limits

Does not derive the eight-tick period from prior axioms.
Does not compute explicit numerical values for any phase.
Does not connect phases to mass formulas or coupling constants.
Does not treat spatial dimensions or the full forcing chain.

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