reals_no_rotation
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that complex numbers are the unique structure capable of encoding rotation.
- Does not quantify rotation angles or connect to specific 8-tick values such as pi/4.
- Does not apply when either factor is zero.
- Does not address multiplication in higher-dimensional division algebras.
formal statement (Lean)
82theorem reals_no_rotation (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) :
83 -- In ℝ: x × y is on the same line as x and y
84 -- No perpendicular component
85 ∃ (s : ℝ), x * y = s * x := by
proof body
Term-mode proof.
86 use y
87 rw [mul_comm]
88
89/-- Complex multiplication includes rotation.
90 z × w rotates z by arg(w) and scales by |w|. -/