QuarticExactZeros.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroZetaContinuation
6 import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Complex
11 
12 theorem quartic_root_square : ((1 + I) / (Real.sqrt 2 : ℂ)) ^ 2 = I := by
13   have hq : (Real.sqrt 2 : ℂ) ^ 2 = 2 := by
14     norm_cast
15     exact Real.sq_sqrt (by norm_num)
16   rw [div_pow, hq, add_sq, I_sq]
17   ring
18 
19 theorem canonicalSignedDenominator_four_eq_cos_cosh (z : ℂ) :
20     canonicalSignedDenominator 4 z = cos (z / (Real.sqrt 2 : ℂ)) * cosh (z / (Real.sqrt 2 : ℂ)) := by
21   have hr : ((1 + I) / (Real.sqrt 2 : ℂ)) ^ 4 = -1 := by
22     rw [show 4 = 2 * 2 by rfl, pow_mul, quartic_root_square, I_sq]
23   rw [canonicalSignedDenominator, entireSigned_independent_roots (by norm_num) (by norm_num)
24     (canonicalPrimitiveRoot_isPrimitive (by norm_num)) isPrimitiveRoot_I
25     (canonicalSignedRoot_pow (by norm_num)) hr, entireSigned_zero_eq_average]
26   norm_num only [Finset.sum_range_succ, Finset.sum_range_zero, pow_zero, pow_one,
27     pow_succ, I_sq, mul_one, zero_add, Nat.cast_ofNat]
28   rw [cos, cosh, div_mul_div_comm, add_mul, mul_add, mul_add]
29   simp only [mul_add, ← exp_add, one_mul, neg_mul]
30   have h1 : (1 + I) / (Real.sqrt 2 : ℂ) * z = z / (Real.sqrt 2 : ℂ) * I + z / (Real.sqrt 2 : ℂ) := by ring
31   have h2 : (1 + I) / (Real.sqrt 2 : ℂ) * I * z = z / (Real.sqrt 2 : ℂ) * I + -(z / (Real.sqrt 2 : ℂ)) := by
32     linear_combination (z / (Real.sqrt 2 : ℂ)) * I_sq
33   have h3 : (1 + I) / (Real.sqrt 2 : ℂ) * (I * I) * z =
34       -(z / (Real.sqrt 2 : ℂ) * I) + -(z / (Real.sqrt 2 : ℂ)) := by
35     rw [I_mul_I]; ring
36   have h4 : (1 + I) / (Real.sqrt 2 : ℂ) * (I * I * I) * z =
37       -(z / (Real.sqrt 2 : ℂ) * I) + z / (Real.sqrt 2 : ℂ) := by
38     rw [I_mul_I]
39     linear_combination -(z / (Real.sqrt 2 : ℂ)) * I_sq
40   rw [h1, h2, h3, h4]
41   ring
42 
43 theorem complex_cos_zero_iff_nat {z : ℂ} :
44     cos z = 0 ↔ ∃ m : ℕ, z = ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) ∨
45       z = -(((m : ℂ) + 1 / 2) * (Real.pi : ℂ)) := by
46   rw [← entireSigned_two_eq_cos (IsPrimitiveRoot.neg_one 0 (by decide)) I_sq]
47   exact entireSigned_two_zero_iff_nat (IsPrimitiveRoot.neg_one 0 (by decide)) I_sq
48 
49 def quarticPositiveZero (m : ℕ) : ℝ := Real.sqrt 2 * Real.pi * ((m : ℝ) + 1 / 2)
50 
51 theorem quarticPositiveZero_pos (m : ℕ) : 0 < quarticPositiveZero m := by
52   unfold quarticPositiveZero
53   positivity
54 
55 theorem quarticPositiveZero_div_sqrt (m : ℕ) :
56     (quarticPositiveZero m : ℂ) / (Real.sqrt 2 : ℂ) =
57       ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) := by
58   have hq : (Real.sqrt 2 : ℂ) ≠ 0 := ofReal_ne_zero.mpr (by positivity)
59   unfold quarticPositiveZero
60   push_cast
61   field_simp
62 
63 theorem canonicalSignedDenominator_four_zero_iff {z : ℂ} :
64     canonicalSignedDenominator 4 z = 0 ↔ ∃ m : ℕ,
65       z = (quarticPositiveZero m : ℂ) ∨ z = -(quarticPositiveZero m : ℂ) ∨
66       z = I * (quarticPositiveZero m : ℂ) ∨ z = -(I * (quarticPositiveZero m : ℂ)) := by
67   have hq : (Real.sqrt 2 : ℂ) ≠ 0 := ofReal_ne_zero.mpr (by positivity)
68   rw [canonicalSignedDenominator_four_eq_cos_cosh, mul_eq_zero, ← cos_mul_I]
69   constructor
70   · intro hz
71     rcases hz with hc | hc
72     · obtain ⟨m, hm | hm⟩ := complex_cos_zero_iff_nat.mp hc
73       · refine ⟨m, Or.inl ?_⟩
74         apply (div_left_inj' hq).mp
75         rw [quarticPositiveZero_div_sqrt, hm]
76       · refine ⟨m, Or.inr (Or.inl ?_)⟩
77         apply (div_left_inj' hq).mp
78         rw [neg_div, quarticPositiveZero_div_sqrt, hm]
79     · obtain ⟨m, hm | hm⟩ := complex_cos_zero_iff_nat.mp hc
80       · refine ⟨m, Or.inr (Or.inr (Or.inr ?_))⟩
81         have h := congrArg (fun w : ℂ => -(w * I)) hm
82         rw [mul_assoc, I_mul_I, mul_neg_one, neg_neg] at h
83         apply (div_left_inj' hq).mp
84         rw [h, neg_div, mul_div_assoc, quarticPositiveZero_div_sqrt]
85         ring
86       · refine ⟨m, Or.inr (Or.inr (Or.inl ?_))⟩
87         have h := congrArg (fun w : ℂ => -(w * I)) hm
88         rw [mul_assoc, I_mul_I, mul_neg_one, neg_neg] at h
89         apply (div_left_inj' hq).mp
90         rw [h, mul_div_assoc, quarticPositiveZero_div_sqrt]
91         ring
92   · rintro ⟨m, hm | hm | hm | hm⟩
93     · left; rw [hm, quarticPositiveZero_div_sqrt]
94       exact complex_cos_zero_iff_nat.mpr ⟨m, Or.inl rfl⟩
95     · left; rw [hm, neg_div, quarticPositiveZero_div_sqrt, cos_neg]
96       exact complex_cos_zero_iff_nat.mpr ⟨m, Or.inl rfl⟩
97     · right
98       rw [hm, mul_div_assoc, quarticPositiveZero_div_sqrt]
99       have he : I * (((m : ℂ) + 1 / 2) * (Real.pi : ℂ)) * I =
100           -(((m : ℂ) + 1 / 2) * (Real.pi : ℂ)) := by
101         linear_combination (((m : ℂ) + 1 / 2) * (Real.pi : ℂ)) * I_sq
102       rw [he, cos_neg]
103       exact complex_cos_zero_iff_nat.mpr ⟨m, Or.inl rfl⟩
104     · right
105       rw [hm, neg_div, mul_div_assoc, quarticPositiveZero_div_sqrt]
106       have he : -(I * (((m : ℂ) + 1 / 2) * (Real.pi : ℂ))) * I =
107           ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) := by
108         linear_combination -(((m : ℂ) + 1 / 2) * (Real.pi : ℂ)) * I_sq
109       rw [he]
110       exact complex_cos_zero_iff_nat.mpr ⟨m, Or.inl rfl⟩
111 
112 theorem quarticPositiveZero_simple (m : ℕ) :
113     analyticOrderAt (canonicalSignedDenominator 4) (quarticPositiveZero m : ℂ) = 1 := by
114   let z : ℂ := quarticPositiveZero m
115   let a : ℂ := Real.sqrt 2
116   have ha : a ≠ 0 := ofReal_ne_zero.mpr (by positivity)
117   have hc : cos (z / a) = 0 := by
118     rw [show z / a = ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) from quarticPositiveZero_div_sqrt m]
119     exact complex_cos_zero_iff_nat.mpr ⟨m, Or.inl rfl⟩
120   have hch : cosh (z / a) ≠ 0 := by
121     rw [show z / a = ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) from quarticPositiveZero_div_sqrt m]
122     have he : ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) = (((m : ℝ) + 1 / 2) * Real.pi : ℝ) := by push_cast; rfl
123     rw [he, ← ofReal_cosh]
124     exact ofReal_ne_zero.mpr (Real.cosh_pos _).ne'
125   have hs : sin (z / a) ≠ 0 := by
126     intro h
127     have he := sin_sq_add_cos_sq (z / a)
128     simp only [h, hc, zero_pow two_ne_zero, zero_add, zero_ne_one] at he
129   have he : canonicalSignedDenominator 4 = fun w => cos (w / a) * cosh (w / a) :=
130     funext canonicalSignedDenominator_four_eq_cos_cosh
131   have hd := ((hasDerivAt_cos (z / a)).comp z ((hasDerivAt_id z).div_const a)).mul
132     ((hasDerivAt_cosh (z / a)).comp z ((hasDerivAt_id z).div_const a))
133   apply (analyticAt_entireSigned 4 0 _ _ _).analyticOrderAt_eq_one_of_zero_deriv_ne_zero
134   · exact canonicalSignedDenominator_four_zero_iff.mpr ⟨m, Or.inl rfl⟩
135   · change deriv (canonicalSignedDenominator 4) z ≠ 0
136     rw [he]
137     erw [hd.deriv]
138     simp only [Function.comp_apply, id_eq, hc, zero_mul, add_zero, one_div]
139     exact mul_ne_zero (mul_ne_zero (neg_ne_zero.mpr hs) (inv_ne_zero ha)) hch
140 
141 theorem canonicalSignedDenominator_four_zero_order_one {z : ℂ}
142     (hz : canonicalSignedDenominator 4 z = 0) :
143     analyticOrderAt (canonicalSignedDenominator 4) z = 1 := by
144   obtain ⟨m, hm | hm | hm | hm⟩ := canonicalSignedDenominator_four_zero_iff.mp hz
145   · rw [hm]; exact quarticPositiveZero_simple m
146   · rw [hm, show -(quarticPositiveZero m : ℂ) = (-1 : ℂ) * (quarticPositiveZero m : ℂ) by ring,
147       ← canonicalSignedDenominator_order_rotation (by norm_num) (show (-1 : ℂ) ^ 4 = 1 by norm_num)]
148     exact quarticPositiveZero_simple m
149   · rw [hm, ← canonicalSignedDenominator_order_rotation (by norm_num) isPrimitiveRoot_I.pow_eq_one]
150     exact quarticPositiveZero_simple m
151   · rw [hm, show -(I * (quarticPositiveZero m : ℂ)) = (-I) * (quarticPositiveZero m : ℂ) by ring,
152       ← canonicalSignedDenominator_order_rotation (by norm_num) isPrimitiveRoot_neg_I.pow_eq_one]
153     exact quarticPositiveZero_simple m
154 
155 end
156 end Komorebi.PaperIV

Back to source controls