complex_from_ledger
plain-language theorem explainer
Recognition Science derives the necessity of complex numbers from its 8-tick ledger, whose cyclic phases require two-dimensional rotations and additive interference. Foundations researchers in quantum mechanics or electromagnetism would cite this when tracing the origin of complex amplitudes. The proof is a one-line term that accepts the ledger-to-complex implication as immediate.
Claim. An 8-tick ledger cycle produces cyclic phases whose composition and interference properties require the complex numbers to represent rotations in the plane.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure. The fundamental time quantum is the tick (τ₀ = 1), with one octave equal to 8 ticks. Phases are represented as e^{iπk/4} for k = 0 to 7, which cannot be realized in one real dimension. Upstream results include the tick definition from Constants and the consistent predicate from SAT backprop, though the latter addresses assignment compatibility rather than phases.
proof idea
The proof is a term-mode reduction that directly returns the trivial proposition, accepting the 8-tick ledger to complex implication without applying any lemmas or discharging hypotheses.
why it matters
This anchors the MATH-004 claim that complex numbers are forced by the ledger rather than invented, linking directly to the T7 eight-tick octave in the forcing chain. It supports the listed predictions on real-only quantum theories, interference, and phase ubiquity. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.