complex_rotation
Complex multiplication combines scaling by the product of moduli with argument addition for nonzero inputs. Researchers deriving the necessity of complex numbers from the 8-tick phase structure would cite this result. The proof is a term-mode split that applies the standard norm-multiplication identity and the coefficient-angle argument-addition lemma.
claimFor $z, w$ in the complex plane, the modulus satisfies $|z w| = |z| |w|$. When both are nonzero, the argument satisfies arg$(z w) =$ arg$(z) +$ arg$(w)$ (modulo $2π$).
background
The module MATH-004 derives the necessity of complex numbers from Recognition Science's 8-tick structure. The upstream EightTick.phase defines the phases as $kπ/4$ for $k$ in Fin 8. The upstream Wedge.phase constructs the unimodular complex number $e^{i w}$. The fundamental tick is the RS time quantum $τ_0 = 1$. Complex numbers supply the 2D rotations needed for these phases.
proof idea
The term proof opens with constructor to split the conjunction. The first conjunct is discharged by direct appeal to the norm-multiplication identity. The second conjunct introduces the nonzero hypotheses and applies the coefficient-angle form of argument multiplication.
why it matters in Recognition Science
This result supplies the rotation property required by the 8-tick octave (T7) in the forcing chain. It supports the module claim that phases are rotations and therefore demand the complex field, feeding the derivation that physics must use ℂ. The theorem closes one step in the argument that 8-tick phases cannot be represented in the reals alone.
scope and limits
- Does not prove that complex numbers are the unique structure supporting these phases.
- Does not address rotations in dimensions higher than two.
- Does not cover cases where one factor is zero.
- Applies only to the standard Euclidean modulus and argument on ℂ.
formal statement (Lean)
91theorem complex_rotation (z w : ℂ) :
92 -- |z × w| = |z| × |w| (scaling)
93 -- arg(z × w) = arg(z) + arg(w) modulo 2π (rotation) when both are nonzero
94 ‖z * w‖ = ‖z‖ * ‖w‖ ∧
95 (∀ hz : z ≠ 0, ∀ hw : w ≠ 0, (Complex.arg (z * w) : Real.Angle) = Complex.arg z + Complex.arg w) := by
proof body
Term-mode proof.
96 constructor
97 · exact Complex.norm_mul z w
98 · intro hz hw
99 -- Use arg_mul_coe_angle which works modulo 2π
100 exact Complex.arg_mul_coe_angle hz hw
101
102/-- **THEOREM**: 8-tick phases require rotation, which requires ℂ.
103 The first non-trivial phase (k=1) has nonzero imaginary part. -/