Theory Third_Unity_Root
theory Third_Unity_Root
imports Complex_Angles
begin
section ‹Third unity root›
text ‹In this section we prove some basic properties of the third unity root j.›
lemma root_unity_3: ‹(z::complex)^3 - 1 = 0 ⟷ (z = cis (2*pi/3) ∨ z=1 ∨ z = cis (4*pi/3))›
proof(rule iffI)
have ‹cis (2 * pi * real xa / 3) ≠ 1 ⟹
cis (2 * pi * real xa / 3) ≠ cis (2 * pi / 3)
⟹ xa < 3 ⟹ cis (2 * pi * real xa / 3) = cis (4 * pi / 3) ›
for xa
proof(rule ccontr)
assume h:‹cis (2 * pi * real xa / 3) ≠ 1›
‹cis (2 * pi * real xa / 3) ≠ cis (2 * pi / 3)›
‹xa < 3› ‹cis (2 * pi * real xa / 3) ≠ cis (4 * pi / 3)›
then have ‹xa = 1 ∨ xa = 0›
using less_Suc_eq numeral_3_eq_3 by fastforce
then show False
using h(1) h(2) by auto
qed
then have f0:‹(λk. cis (2 * pi * real k / real 3)) ` {..<3} = {1, cis(2*pi/3), cis (4*pi/3)}›
unfolding image_def by(auto simp: image_def intro:bexI[where x=0]
bexI[where x=1] bexI[where x=2])
have ‹{z. z^3 = 1} = {1, cis(2*pi/3), cis (4*pi/3)}›
apply(insert bij_betw_roots_unity[of 3, simplified])
apply(frule bij_betw_imp_surj_on)
using f0 by auto
then show ‹z ^ 3 - 1 = 0 ⟹ z = cis (2 * pi / 3) ∨ z = 1 ∨ z = cis (4 * pi / 3)›
unfolding bij_betw_def inj_on_def by(auto)
show ‹ z = cis (2 * pi / 3) ∨ z = 1 ∨ z = cis (4 * pi / 3) ⟹ z ^ 3 - 1 = 0 ›
using cis_2pi cis_multiple_2pi[of 2] by(auto simp:DeMoivre field_simps)
qed
definition root3 where ‹root3≡cis(2*pi/3)›
lemma root3_eq_0:‹1 + root3 + root3^2 = 0›
proof -
have ‹(z::complex)^3 - 1 = (z - 1)*(1 + z + z^2)› for z
by(auto simp:field_simps power2_eq_square power3_eq_cube)
moreover have ‹root3^3 - 1 = 0›
using root_unity_3 unfolding root3_def by blast
moreover have ‹root3-1 ≠ 0›
by(simp add:cis.code Complex_eq_1 cos_120 root3_def)
ultimately show ?thesis
by simp
qed
lemma root_unity_carac:
assumes h1:‹a1*a2*a3 = j› ‹1-a1*a2 ≠ 0 ∧ 1-a2*a3≠0 ∧ 1-a1*a3 ≠ 0› ‹j=root3›
and R : ‹R=(a1 * b2 + b1) / (1 - a1 * a2)› (is ‹R=?R›)
and P :‹P=(a2*b3 + b2)/(1-a2*a3)› (is ‹P=?P›)
and Q:‹Q=(a3*b1 + b3)/(1-a3*a1)› (is ‹Q=?Q›)
shows ‹(a1^2+a1+1)*b1 + a1^3*(a2^2+a2+1)*b2 +a1^3*a2^3*(a3^2+a3+1)*b3 =
-j*a1^2*a2*(a1-j)*(a2-j)*(a3-j)*(?R +j*?P +j^2*?Q)›
proof -
have simp_rules_for_eq:‹1-a1*a2 ≠ 0 ∧ 1-a2*a3≠0 ∧ 1-a1*a3 ≠ 0› ‹a1*a2*a3 = j›
‹1 + j +j^2 = 0› ‹j*j*j = 1› ‹(1-a1*a2)*a3 = (a3-j)› ‹(1-a2*a3)*a1 = (a1-j)› ‹(1-a1*a3)*a2 = (a2-j)›
using h1 root3_eq_0 root_unity_3 unfolding root3_def
by(auto simp:power3_eq_cube mult.left_commute mult.commute right_diff_distrib)
have y:‹ (- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) *
(a1 * b2) + - j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * b1) /
(1 - a1 * a2) = (- j * a1⇧2 * a2 * ((1 - a3 * a2) * a1) * ((1 - a1 * a3) * a2) * ( a3) * (a1 * b2)
+ - j * a1⇧2 * a2 * ((1 - a3 * a2) * a1) * ((1 - a1 * a3) * a2) * (a3) * b1)›
apply(subst add_divide_distrib)
using simp_rules_for_eq(1)
by (simp add: mult.commute)
have y2:‹(- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * (j * (a2 * b3)) +
- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * (j * b2)) /
(1 - a2 * a3) = (- j * a1⇧2 * a2 * (a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * (j * (a2 * b3)) +
- j * a1⇧2 * a2 * (a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * (j * b2))›
apply(subst add_divide_distrib)
using simp_rules_for_eq(1) by auto
have y3:‹(- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * (j⇧2 * (a3 * b1)) +
- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * ((1 - a1 * a3) * a2) * ((1 - a1 * a2) * a3) * (j⇧2 * b3)) /
(1 - a3 * a1) =
(- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * (a2) * ((1 - a1 * a2) * a3) * (j⇧2 * (a3 * b1)) +
- j * a1⇧2 * a2 * ((1 - a2 * a3) * a1) * (a2) * ((1 - a1 * a2) * a3) * (j⇧2 * b3))›
apply(subst add_divide_distrib)
by (smt (verit, best) mult.commute nonzero_mult_div_cancel_left times_divide_eq_left simp_rules_for_eq(1))
have ko:‹a*(b*(c)) = a*b*c› for a b c::complex
by auto
have ko':‹a +(b +(c)) = a+b+c› for a b c::complex
by auto
have *:‹a1 * a1 * a1 * a1 * a1 * a2 * a2 * a2 * a2 * a3 * a3 * a3 * a3 * b1 = a1*a1*a2*a3*b1›
using simp_rules_for_eq by (auto simp add: mult.assoc mult.left_commute)
have **:‹a1 * a1 * a1 * a1 * a1 * a2 * a2 * a2 * a2 * a2 * a3 * a3 * a3 * b3 = a1*a1*a2*a2*b3›
using simp_rules_for_eq by (auto simp add: mult.assoc mult.left_commute)
have ***:‹a1 * a1 * a1 * a1 * a1 * a1 * a2 * a2 * a2 * a2 * a2 * a3 * a3 * a3 * a3 * b3
= a1*a1*a1*a2*a2*a3*b3›
using simp_rules_for_eq by (auto simp add: mult.assoc mult.left_commute)
have fin:‹a1 * b1 + a1 * a1 * a1 * a2 * b2 + a1 * a1 * a1 * a1 * a2 * a2 * a3 * b2 +
a1 * a1 * a1 * a2 * a2 * a2 * a3 * b3 + a1 * a1 * a1 * a2 * a2 * a3 * a3 * b1 +
a1 * a1 * a1 * a1 * a1 * a2 * a2 * a2 * a3 * a3 * b2 +a1 * a1 * a1 * a1 * a2 * a2 * a2 * a2 *
a3 * a3 * b3 + a1 * a1 * a2 * a2 * b3 + a1 * a1 * a2 * a3 * b1 = a1*b1 + j*a1*b1 + j^2*a1*b1 +
a1*a1*a1*a2*b2 + a1*a1*a1*a2*b2*j + a1*a1*a1*a2*b2*j^2 + a1*a1*a2*a2*b3 + a1*a1*a2*a2*b3*j +
a1*a1*a2*a2*b3*j^2›
using simp_rules_for_eq by(auto simp:algebra_simps power2_eq_square power3_eq_cube)
then have fin':‹… = (a1*b1 + a1*a1*a1*a2*b2 + a1*a1*a2*a2*b3)*(1+j+j^2)›
by(auto simp:algebra_simps power2_eq_square power3_eq_cube)
then show graal:‹(a1^2+a1+1)*b1 + a1^3*(a2^2+a2+1)*b2 +a1^3*a2^3*(a3^2+a3+1)*b3 =
-j*a1^2*a2*(a1-j)*(a2-j)*(a3-j)*(?R +j*?P +j^2*?Q)›
apply(simp only: simp_rules_for_eq(5-7)[symmetric])
apply(simp only:y y2 y3 distrib_left distrib_right times_divide_eq_left times_divide_eq_right)
apply(simp only:simp_rules_for_eq algebra_simps del:mult.assoc mult.commute)
apply(simp only:ko ko')
using simp_rules_for_eq apply(auto simp add: power2_eq_square power3_eq_cube algebra_simps)
apply(simp only:ko ko') apply(subst *) apply(subst **) apply(subst ***) apply(simp)
apply(simp only:ko ko') apply(subst fin) apply(subst fin')
using simp_rules_for_eq by fastforce
qed
end