ComplexFalsifier
plain-language theorem explainer
ComplexFalsifier packages candidate challenges to the necessity of complex numbers arising from the eight-tick phase cycle. A foundations physicist would cite it when cataloguing constraints on real-only formulations of quantum mechanics or phase-free dynamics. The declaration is a direct structure definition that introduces two string fields with no further computation or lemmas.
Claim. A record type whose instances consist of a descriptive string naming a potential falsifier together with a status string recording its current standing.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's eight-tick structure. Each tick advances by a 45-degree rotation, so the full cycle requires representation in a two-dimensional plane; one dimension cannot support nontrivial rotations. Upstream structures supply the discrete ledger factorization, J-cost convexity, and spectral emergence that fix the eight phases and force the use of the imaginary unit for their encoding.
proof idea
The declaration is a direct structure definition with two string fields. No lemmas or tactics are invoked; the body simply declares the fields falsifier and status.
why it matters
The structure feeds the experimentalStatus list that enumerates ruled-out alternatives such as real-only quantum mechanics. It completes the MATH-004 argument that the eight-tick octave (T7) and the two-dimensional rotation requirement together force complex numbers into the formalism. The definition touches the open question of whether any consistent phase-free formulation of the ledger dynamics exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.