experimentalStatus
plain-language theorem explainer
Physicists studying quantum foundations cite this definition when summarizing experimental support for complex numbers required by the 8-tick phase cycle. It assembles three observations that real-only QM fails, phases are essential, and the 8-tick appears in spin statistics. The definition builds the list by direct construction of three ComplexFalsifier records.
Claim. The experimental status is the list whose entries are the pairs (``Real QM'', ``Ruled out by Renou et al. (2021)''), (``Phase in experiments'', ``Ubiquitous and essential''), and (``8-tick structure'', ``Appears in spin statistics''), where each pair records a candidate falsifier of complex-number necessity together with its observed status.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure. Phases at multiples of 45 degrees are rotations and therefore require a two-dimensional representation supplied by the complex numbers. ComplexFalsifier is the record type whose fields are a string naming a potential falsifier and a string describing its status. The upstream definition of tick supplies the fundamental time quantum while Phase is the type Fin 8 indexing the eight phases in one cycle.
proof idea
This definition is a direct list literal. It constructs three instances of the ComplexFalsifier structure and assembles them into a List. No external lemmas or tactics are invoked.
why it matters
This definition supplies the concrete evidence list for the complex-numbers necessity argument in the MATH-004 module. It records that real-only quantum mechanics is ruled out by experiment and that phases are ubiquitous, thereby reinforcing the link from the eight-tick octave (T7) to the requirement for complex arithmetic. The entry on 8-tick structure appearing in spin statistics ties directly to the forcing-chain landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.