DyadicFourPrefix.lean

1 module
2 
3 public import DyadicFourAllRows
4 public import DyadicLogThresholds
5 
6 /-!
7 Exact initial Newton coefficients for the four normalized generalized Euler
8 packets. Every displayed rational is derived from the defining triangular
9 recurrence. Their valuations, together with the checked all-order dyadic bound,
10 prove the uniform tail estimate needed for exact displacement valuations.
11 The finite prefix is part of a universal proof, not a sampled surrogate.
12 -/
13 
14 @[expose] public section
15 noncomputable section
16 set_option autoImplicit false
17 set_option maxRecDepth 4096
18 set_option maxHeartbeats 800000
19 
20 namespace KomorebiPaperIX.DyadicFourPrefix
21 
22 open Mahler Congruential
23 
24 /-- Valuation of the first normalized Newton coefficient, for j < 4. -/
25 def bonus (j : ℕ) : ℕ := match j with
26   | 0 => 1
27   | 1 => 1
28   | 2 => 4
29   | _ => 2
30 
31 def mahlerCoeff (j k : ℕ) : ℚ := Mahler.coefficient (coeff 4 j) k
32 
33 theorem coeff_0_1 : coeff 4 0 1 = (-1/1:ℚ) := by
34   rw [coefficient_recurrence 4 0 (by decide : 0 < 1)]
35   norm_num [Finset.sum_range_succ, Nat.choose]
36 
37 theorem coeff_0_2 : coeff 4 0 2 = (69/1:ℚ) := by
38   rw [coefficient_recurrence 4 0 (by decide : 0 < 2)]
39   norm_num [Finset.sum_range_succ, Nat.choose, coeff_0_1]
40 
41 theorem mahler_0_1 : mahlerCoeff 0 1 = (-2/1:ℚ) := by
42   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_0_1]
43 
44 theorem mahler_0_2 : mahlerCoeff 0 2 = (72/1:ℚ) := by
45   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_0_1, coeff_0_2]
46 
47 theorem coeff_1_1 : coeff 4 1 1 = (-1/5:ℚ) := by
48   rw [coefficient_recurrence 4 1 (by decide : 0 < 1)]
49   norm_num [Finset.sum_range_succ, Nat.choose]
50 
51 theorem coeff_1_2 : coeff 4 1 2 = (121/45:ℚ) := by
52   rw [coefficient_recurrence 4 1 (by decide : 0 < 2)]
53   norm_num [Finset.sum_range_succ, Nat.choose, coeff_1_1]
54 
55 theorem mahler_1_1 : mahlerCoeff 1 1 = (-6/5:ℚ) := by
56   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_1_1]
57 
58 theorem mahler_1_2 : mahlerCoeff 1 2 = (184/45:ℚ) := by
59   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_1_1, coeff_1_2]
60 
61 theorem coeff_2_1 : coeff 4 2 1 = (-1/15:ℚ) := by
62   rw [coefficient_recurrence 4 2 (by decide : 0 < 1)]
63   norm_num [Finset.sum_range_succ, Nat.choose]
64 
65 theorem coeff_2_2 : coeff 4 2 2 = (13/45:ℚ) := by
66   rw [coefficient_recurrence 4 2 (by decide : 0 < 2)]
67   norm_num [Finset.sum_range_succ, Nat.choose, coeff_2_1]
68 
69 theorem coeff_2_3 : coeff 4 2 3 = (-4009/455:ℚ) := by
70   rw [coefficient_recurrence 4 2 (by decide : 0 < 3)]
71   norm_num [Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2]
72 
73 theorem coeff_2_4 : coeff 4 2 4 = (151129/153:ℚ) := by
74   rw [coefficient_recurrence 4 2 (by decide : 0 < 4)]
75   norm_num [Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3]
76 
77 theorem coeff_2_5 : coeff 4 2 5 = (-340474381/1155:ℚ) := by
78   rw [coefficient_recurrence 4 2 (by decide : 0 < 5)]
79   norm_num [Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3, coeff_2_4]
80 
81 theorem coeff_2_6 : coeff 4 2 6 = (790092547807/4095:ℚ) := by
82   rw [coefficient_recurrence 4 2 (by decide : 0 < 6)]
83   norm_num [Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3, coeff_2_4, coeff_2_5]
84 
85 theorem mahler_2_1 : mahlerCoeff 2 1 = (-16/15:ℚ) := by
86   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_2_1]
87 
88 theorem mahler_2_2 : mahlerCoeff 2 2 = (64/45:ℚ) := by
89   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2]
90 
91 theorem mahler_2_3 : mahlerCoeff 2 3 = (-14848/1365:ℚ) := by
92   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3]
93 
94 theorem mahler_2_4 : mahlerCoeff 2 4 = (71426048/69615:ℚ) := by
95   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3, coeff_2_4]
96 
97 theorem mahler_2_5 : mahlerCoeff 2 5 = (-25509691392/85085:ℚ) := by
98   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3, coeff_2_4, coeff_2_5]
99 
100 theorem mahler_2_6 : mahlerCoeff 2 6 = (149113198870528/765765:ℚ) := by
101   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_2_1, coeff_2_2, coeff_2_3, coeff_2_4, coeff_2_5, coeff_2_6]
102 
103 theorem coeff_3_1 : coeff 4 3 1 = (-1/35:ℚ) := by
104   rw [coefficient_recurrence 4 3 (by decide : 0 < 1)]
105   norm_num [Finset.sum_range_succ, Nat.choose]
106 
107 theorem coeff_3_2 : coeff 4 3 2 = (59/1155:ℚ) := by
108   rw [coefficient_recurrence 4 3 (by decide : 0 < 2)]
109   norm_num [Finset.sum_range_succ, Nat.choose, coeff_3_1]
110 
111 theorem coeff_3_3 : coeff 4 3 3 = (-407/637:ℚ) := by
112   rw [coefficient_recurrence 4 3 (by decide : 0 < 3)]
113   norm_num [Finset.sum_range_succ, Nat.choose, coeff_3_1, coeff_3_2]
114 
115 theorem coeff_3_4 : coeff 4 3 4 = (15330979/522291:ℚ) := by
116   rw [coefficient_recurrence 4 3 (by decide : 0 < 4)]
117   norm_num [Finset.sum_range_succ, Nat.choose, coeff_3_1, coeff_3_2, coeff_3_3]
118 
119 theorem mahler_3_1 : mahlerCoeff 3 1 = (-36/35:ℚ) := by
120   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_3_1]
121 
122 theorem mahler_3_2 : mahlerCoeff 3 2 = (256/231:ℚ) := by
123   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_3_1, coeff_3_2]
124 
125 theorem mahler_3_3 : mahlerCoeff 3 3 = (-65792/35035:ℚ) := by
126   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_3_1, coeff_3_2, coeff_3_3]
127 
128 theorem mahler_3_4 : mahlerCoeff 3 4 = (161644544/4849845:ℚ) := by
129   norm_num [mahlerCoeff, Mahler.coefficient, difference_explicit, Finset.sum_range_succ, Nat.choose, coeff_3_1, coeff_3_2, coeff_3_3, coeff_3_4]
130 
131 theorem valuation_two_power_odd (e u : ℕ) (hu : ¬ 2 ∣ u) :
132     padicValNat 2 (2^e*u) = e := by
133   have hu0 : u ≠ 0 := by intro h; exact hu (h ▸ dvd_zero 2)
134   rw [padicValNat.mul (by positivity) hu0, padicValNat.prime_pow,
135     padicValNat.eq_zero_of_not_dvd hu, Nat.add_zero]
136 
137 theorem mahler_valuation_0_1 : padicValRat 2 (mahlerCoeff 0 1) = 1 := by
138   have hv : padicValNat 2 2 = 1 := by
139     rw [show (2:ℕ) = 2^1*1 by norm_num]
140     exact valuation_two_power_odd 1 1 (by norm_num)
141   rw [mahler_0_1]
142   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
143 
144 theorem mahler_valuation_0_2 : padicValRat 2 (mahlerCoeff 0 2) = 3 := by
145   have hv : padicValNat 2 72 = 3 := by
146     rw [show (72:ℕ) = 2^3*9 by norm_num]
147     exact valuation_two_power_odd 3 9 (by norm_num)
148   rw [mahler_0_2]
149   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
150 
151 theorem mahler_valuation_1_1 : padicValRat 2 (mahlerCoeff 1 1) = 1 := by
152   have hv : padicValNat 2 6 = 1 := by
153     rw [show (6:ℕ) = 2^1*3 by norm_num]
154     exact valuation_two_power_odd 1 3 (by norm_num)
155   rw [mahler_1_1]
156   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
157 
158 theorem mahler_valuation_1_2 : padicValRat 2 (mahlerCoeff 1 2) = 3 := by
159   have hv : padicValNat 2 184 = 3 := by
160     rw [show (184:ℕ) = 2^3*23 by norm_num]
161     exact valuation_two_power_odd 3 23 (by norm_num)
162   rw [mahler_1_2]
163   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
164 
165 theorem mahler_valuation_2_1 : padicValRat 2 (mahlerCoeff 2 1) = 4 := by
166   have hv : padicValNat 2 16 = 4 := by
167     rw [show (16:ℕ) = 2^4*1 by norm_num]
168     exact valuation_two_power_odd 4 1 (by norm_num)
169   rw [mahler_2_1]
170   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
171 
172 theorem mahler_valuation_2_2 : padicValRat 2 (mahlerCoeff 2 2) = 6 := by
173   have hv : padicValNat 2 64 = 6 := by
174     rw [show (64:ℕ) = 2^6*1 by norm_num]
175     exact valuation_two_power_odd 6 1 (by norm_num)
176   rw [mahler_2_2]
177   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
178 
179 theorem mahler_valuation_2_3 : padicValRat 2 (mahlerCoeff 2 3) = 9 := by
180   have hv : padicValNat 2 14848 = 9 := by
181     rw [show (14848:ℕ) = 2^9*29 by norm_num]
182     exact valuation_two_power_odd 9 29 (by norm_num)
183   rw [mahler_2_3]
184   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
185 
186 theorem mahler_valuation_2_4 : padicValRat 2 (mahlerCoeff 2 4) = 13 := by
187   have hv : padicValNat 2 71426048 = 13 := by
188     rw [show (71426048:ℕ) = 2^13*8719 by norm_num]
189     exact valuation_two_power_odd 13 8719 (by norm_num)
190   rw [mahler_2_4]
191   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
192 
193 theorem mahler_valuation_2_5 : padicValRat 2 (mahlerCoeff 2 5) = 16 := by
194   have hv : padicValNat 2 25509691392 = 16 := by
195     rw [show (25509691392:ℕ) = 2^16*389247 by norm_num]
196     exact valuation_two_power_odd 16 389247 (by norm_num)
197   rw [mahler_2_5]
198   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
199 
200 theorem mahler_valuation_2_6 : padicValRat 2 (mahlerCoeff 2 6) = 22 := by
201   have hv : padicValNat 2 149113198870528 = 22 := by
202     rw [show (149113198870528:ℕ) = 2^22*35551357 by norm_num]
203     exact valuation_two_power_odd 22 35551357 (by norm_num)
204   rw [mahler_2_6]
205   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
206 
207 theorem mahler_valuation_3_1 : padicValRat 2 (mahlerCoeff 3 1) = 2 := by
208   have hv : padicValNat 2 36 = 2 := by
209     rw [show (36:ℕ) = 2^2*9 by norm_num]
210     exact valuation_two_power_odd 2 9 (by norm_num)
211   rw [mahler_3_1]
212   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
213 
214 theorem mahler_valuation_3_2 : padicValRat 2 (mahlerCoeff 3 2) = 8 := by
215   have hv : padicValNat 2 256 = 8 := by
216     rw [show (256:ℕ) = 2^8*1 by norm_num]
217     exact valuation_two_power_odd 8 1 (by norm_num)
218   rw [mahler_3_2]
219   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
220 
221 theorem mahler_valuation_3_3 : padicValRat 2 (mahlerCoeff 3 3) = 8 := by
222   have hv : padicValNat 2 65792 = 8 := by
223     rw [show (65792:ℕ) = 2^8*257 by norm_num]
224     exact valuation_two_power_odd 8 257 (by norm_num)
225   rw [mahler_3_3]
226   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
227 
228 theorem mahler_valuation_3_4 : padicValRat 2 (mahlerCoeff 3 4) = 15 := by
229   have hv : padicValNat 2 161644544 = 15 := by
230     rw [show (161644544:ℕ) = 2^15*4933 by norm_num]
231     exact valuation_two_power_odd 15 4933 (by norm_num)
232   rw [mahler_3_4]
233   norm_num [padicValRat_def, padicValInt, hv, padicValNat.eq_zero_of_not_dvd]
234 
235 theorem first_nonzero (j : ℕ) (hj : j < 4) : mahlerCoeff j 1 ≠ 0 := by
236   interval_cases j <;> norm_num [mahler_0_1, mahler_1_1, mahler_2_1, mahler_3_1]
237 
238 theorem first_valuation (j : ℕ) (hj : j < 4) :
239     padicValRat 2 (mahlerCoeff j 1) = (bonus j : ℤ) := by
240   interval_cases j <;>
241     norm_num [mahler_valuation_0_1, mahler_valuation_1_1,
242       mahler_valuation_2_1, mahler_valuation_3_1, bonus]
243 
244 theorem precision_of_order_le (j k L : ℕ) (hj : j < 4) (hL : L ≤ k) :
245     GlobalEulerBoundary.precision 2 (L:ℤ) (mahlerCoeff j k) := by
246   have H := DyadicFourAllRows.normalized_precision j 1 k 0 hj
247   rcases H with hz | hv
248   · exact Or.inl hz
249   · exact Or.inr (le_trans (by exact_mod_cast hL) hv)
250 
251 /-- All higher Newton terms have the extra precision needed for first-term dominance. -/
252 theorem tail_precision (j : ℕ) (hj : j < 4) (k : ℕ) (hk : 2 ≤ k) :
253     GlobalEulerBoundary.precision 2 ((bonus j + 1 + Nat.log 2 k : ℕ):ℤ)
254       (mahlerCoeff j k) := by
255   interval_cases j
256   · by_cases hlarge : 3 ≤ k
257     · apply precision_of_order_le 0 k _ (by decide)
258       simpa [bonus] using DyadicLogThresholds.two_add_log_le k hlarge
259     · have he : k = 2 := by omega
260       subst k
261       apply Or.inr
262       rw [mahler_valuation_0_2]
263       decide
264   · by_cases hlarge : 3 ≤ k
265     · apply precision_of_order_le 1 k _ (by decide)
266       simpa [bonus] using DyadicLogThresholds.two_add_log_le k hlarge
267     · have he : k = 2 := by omega
268       subst k
269       apply Or.inr
270       rw [mahler_valuation_1_2]
271       decide
272   · by_cases hlarge : 7 ≤ k
273     · apply precision_of_order_le 2 k _ (by decide)
274       simpa [bonus] using DyadicLogThresholds.five_add_log_le k hlarge
275     · interval_cases k <;> apply Or.inr
276       all_goals first
277         | rw [mahler_valuation_2_2]; decide
278         | rw [mahler_valuation_2_3]; decide
279         | rw [mahler_valuation_2_4]; decide
280         | rw [mahler_valuation_2_5]; decide
281         | rw [mahler_valuation_2_6]; decide
282   · by_cases hlarge : 5 ≤ k
283     · apply precision_of_order_le 3 k _ (by decide)
284       simpa [bonus] using DyadicLogThresholds.three_add_log_le k hlarge
285     · interval_cases k <;> apply Or.inr
286       all_goals first
287         | rw [mahler_valuation_3_2]; decide
288         | rw [mahler_valuation_3_3]; decide
289         | rw [mahler_valuation_3_4]; decide
290 
291 end KomorebiPaperIX.DyadicFourPrefix

Back to source controls