complex_rotation
plain-language theorem explainer
Complex multiplication on ℂ multiplies moduli and adds arguments (modulo 2π) for nonzero inputs. Researchers deriving the necessity of complex numbers from the 8-tick ledger cycle cite this when showing that phases cannot be realized in ℝ alone. The proof is a direct term-mode application of the standard norm and argument lemmas from Mathlib.
Claim. For $z, w ∈ ℂ$, $|z w| = |z| |w|$. When $z ≠ 0$ and $w ≠ 0$, the argument satisfies arg$(z w) =$ arg$(z) +$ arg$(w)$ (modulo $2π$, as an element of Real.Angle).
background
The module MATH-004 derives the necessity of ℂ from the 8-tick structure: the ledger cycle has eight phases at angles $kπ/4$ for $k=0..7$, each a 45° rotation. Upstream, Foundation.EightTick.phase defines these as $(k:ℝ)·π/4$, while NumberTheory.RiemannHypothesis.Wedge.phase supplies the unimodular complex representative $e^{i w}$. Constants.tick supplies the base time quantum whose octave is period 8. The present theorem records the algebraic fact that multiplication in ℂ simultaneously scales lengths and adds angles, the precise operation needed to realize those phases.
proof idea
The term proof opens with constructor to split the conjunction. The left conjunct is discharged by the exact application of Complex.norm_mul. The right conjunct is discharged by an intro of the two nonzero hypotheses followed by exact Complex.arg_mul_coe_angle, which returns the sum inside Real.Angle.
why it matters
This supplies the rotation property required by the module's core claim that 8-tick phases (T7 of the forcing chain) force a two-dimensional representation and therefore ℂ. It sits immediately before the sibling results phases_require_complex and quantum_requires_complex, which close the argument that the ledger structure cannot be embedded in ℝ. The result therefore anchors the paper proposition that complex numbers appear in physics because the fundamental cycle is an eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.