pith. sign in
theorem

quantum_requires_complex

proved
show as:
module
IndisputableMonolith.Mathematics.ComplexNumbers
domain
Mathematics
line
164 · github
papers citing
none yet

plain-language theorem explainer

Quantum mechanics requires complex numbers in its wavefunction formulation because Bell-like experiments distinguish real from complex versions and confirm the complex case. Foundations researchers would cite this when ruling out real-valued alternatives to the Schrödinger equation. The proof is a term-mode reduction to the trivial proposition.

Claim. Quantum mechanics requires a complex-valued wavefunction, as Bell-like experiments distinguish real versus complex formulations and experimental results confirm the complex case.

background

The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure: the fundamental ledger cycle has eight phases at 45° intervals, represented by roots of unity $e^{iπk/4}$, which cannot be realized in one real dimension. Upstream results supply concrete experimental lists confirming quantum behavior, including fullerene interference, LIGO mirror noise limits, double-slit diffraction with electrons and fullerenes, and neutrino oscillation measurements from DUNE and Hyper-Kamiande. These lists stand in for the empirical support that complex quantum mechanics is required.

proof idea

The declaration is a term-mode proof that applies the trivial tactic directly to the proposition True.

why it matters

This theorem fills the quantum-mechanics slot in the MATH-004 derivation that complex numbers follow from the eight-tick octave (T7) and the requirement of planar rotations. It is cited by the module's core insight that physics must use ℂ because the ledger has phases, and it references the 2021 result that no real formulation works. No downstream uses are recorded, leaving open how this interfaces with the Schrödinger equation or phasor definitions elsewhere in the module.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.