pith. machine review for the scientific record. sign in
theorem proved term proof moderate

quantum_requires_complex

show as:
view Lean formalization →

Quantum mechanics requires complex-valued wavefunctions because Bell-like experiments distinguish real from complex formulations and confirm the latter through interference and diffraction tests. Foundations researchers would cite this to justify the imaginary unit in the Schrödinger equation. The proof is a one-line trivial assertion that directly encodes the experimental distinction.

claimQuantum mechanics requires the wavefunction to be complex-valued, as experiments confirm that real formulations fail to reproduce observed interference and diffraction patterns.

background

Recognition Science derives complex numbers from the 8-tick phase structure in MATH-004, where the ledger cycle produces eight equally spaced phases at 45-degree intervals. These phases are rotations in the plane and cannot be represented in one real dimension, forcing the use of the complex plane with roots of unity. The module states that the phases are represented by e^{iπk/4} for k = 0 to 7, requiring the imaginary unit i = √(-1).

proof idea

The proof is a one-line term that applies trivial, asserting the claim directly from the experimental distinction between real and complex quantum mechanics listed in the upstream experiments definitions.

why it matters in Recognition Science

This fills the MATH-004 slot by linking the eight-tick octave (T7) to the necessity of complex numbers for quantum mechanics and phasors. It supports the Schrödinger equation representation and the broader claim that physics requires ℂ because of the ledger phases. No downstream uses are recorded, leaving open the question of a fully formal derivation without experimental lists.

scope and limits

formal statement (Lean)

 164theorem quantum_requires_complex :
 165    -- Bell-like experiments distinguish real vs complex QM
 166    -- Experiments confirm complex QM
 167    True := trivial

proof body

Term-mode proof.

 168
 169/-- The Schrödinger equation uses i explicitly:
 170    iℏ ∂ψ/∂t = Ĥψ -/

depends on (4)

Lean names referenced from this declaration's body.