ComplexFalsifier
plain-language theorem explainer
A structure records candidate counterexamples that would falsify the claim that eight-tick phases force complex numbers in physics. Researchers examining the foundations of quantum mechanics or phase-sensitive measurements would reference the listed conditions when testing necessity of the imaginary unit. The declaration is a direct two-field structure with no proof obligations or computational content.
Claim. A record type consisting of a string naming a potential falsifier together with a string recording its status, for the claim that the eight-tick phase cycle (rotations by multiples of $45^circ$) necessitates the complex numbers.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's eight-tick ledger cycle. Each tick corresponds to a $45^circ$ rotation, so the eight phases are the eighth roots of unity; these rotations cannot be represented in one real dimension and therefore require the plane identified with the complex numbers. The structure ComplexFalsifier enumerates the observations that would break this chain: real-only quantum mechanics, absence of phases, an alternative to the eight-tick structure, or rotation possible in fewer than two dimensions.
proof idea
Direct structure definition introducing the two String fields; no lemmas or tactics are applied.
why it matters
The definition supplies the type used by experimentalStatus to list concrete evidence (Renou et al. 2021 ruling out real QM, ubiquitous phases, spin statistics) that supports the complex-necessity claim. It therefore closes the falsification side of the argument that begins from the eight-tick octave (T7) and the requirement that phases be rotations in two dimensions. The parent result is the overall derivation in the module that complex numbers appear in quantum mechanics, electromagnetism and Fourier analysis because the ledger itself is eight-tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.