Trigonometric Identities from Complex Multiplication¶
Euler's formula packages cosine and sine into one algebraic object,
$$u(\alpha)=\cos\alpha+i\sin\alpha=e^{i\alpha}.$$
Multiplying these objects lets the real and imaginary coefficients reveal several familiar identities. This is a useful symbolic-computation pattern: perform one polynomial calculation and interpret its coefficients.
Symbolic unit-circle elements¶
We keep $\alpha$ and $\beta$ symbolic. The expression uMinusBeta
represents $u(-\beta)=\cos\beta-i\sin\beta$ without asking the
simplifier to know parity rules for sine and cosine.
declare symbol α, β : MathValue
def uAlpha : MathValue := cos α + i * sin α
def uBeta : MathValue := cos β + i * sin β
def uMinusBeta : MathValue := cos β - i * sin β
Angle-addition formulas¶
The coefficients of $1$ and $i$ in $u(\alpha)u(\beta)$ are, respectively, $\cos(\alpha+\beta)$ and $\sin(\alpha+\beta)$.
coefficients (uAlpha * uBeta) i
Reading the two returned coefficients gives
$$ \cos(\alpha+\beta)=\cos\alpha\cos\beta-\sin\alpha\sin\beta, $$ $$ \sin(\alpha+\beta)=\sin\alpha\cos\beta+\cos\alpha\sin\beta. $$
Adding $u(\alpha)u(\beta)$ and $u(\alpha)u(-\beta)$ isolates the product-to-sum combinations.
coefficients (uAlpha * uBeta + uAlpha * uMinusBeta) i
The result encodes $2\cos\alpha\cos\beta$ in its real part and $2\sin\alpha\cos\beta$ in its imaginary part. Dividing by two and replacing the two products by $u(\alpha\pm\beta)$ yields the standard product-to-sum identities.
Triple-angle formulas¶
Cubing one unit-circle element performs all terms of the binomial expansion at once.
coefficients (uAlpha ^ 3) i
The real and imaginary components are
$$\cos^3\alpha-3\cos\alpha\sin^2\alpha,$$ $$3\cos^2\alpha\sin\alpha-\sin^3\alpha.$$
Using $\sin^2\alpha=1-\cos^2\alpha$ in the first and $\cos^2\alpha=1-\sin^2\alpha$ in the second gives
$$\cos(3\alpha)=4\cos^3\alpha-3\cos\alpha,$$ $$\sin(3\alpha)=3\sin\alpha-4\sin^3\alpha.$$
The essential point is that Egison's coefficient extraction turns complex multiplication into a transparent derivation, rather than merely checking a pre-stated identity.