reals_no_rotation
plain-language theorem explainer
Real multiplication of nonzero scalars x and y produces only a scaled copy along the same line, with no perpendicular component. Researchers deriving the necessity of complex numbers from Recognition Science's 8-tick phase structure cite this to contrast real scaling against rotational multiplication in C. The proof is a one-line term proof that instantiates the existential witness with y and rewrites via commutativity of real multiplication.
Claim. For all nonzero real numbers $x$ and $y$, there exists a real scalar $s$ such that $x y = s x$.
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick phase structure. Each tick corresponds to a 45-degree rotation in the fundamental ledger cycle, so phases must be represented by elements of the form $e^{i k pi /4}$. Real numbers supply only scaling and cannot encode these rotations, as stated in the declaration's doc-comment: multiplication in R is just scaling with no rotation.
proof idea
The proof is a one-line term proof. It applies the tactic use y to supply the existential witness, then rewrites with mul_comm to obtain the required equality.
why it matters
This result shows the absence of rotational degrees of freedom in the reals and thereby supports the module's claim that the 8-tick octave forces complex structure for phase representation. It precedes sibling declarations such as complex_rotation and phases_require_complex, which complete the argument that physics requires C because of the ledger's eight phases. The declaration touches the foundational question of why complex numbers appear in quantum mechanics and electromagnetism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.