Skip to content

Commit bf047df

Browse files
Chessing234Chessing234
committed
proof: certify exact first descent, crossing gaps, and audit 12012 theorems
1 parent 0a5c587 commit bf047df

11 files changed

Lines changed: 44350 additions & 1 deletion

‎Collatz/Research/FirstDescent/All.lean‎

Lines changed: 300 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,300 @@
1+
import Collatz.Research.FirstDescent.Batch001
2+
import Collatz.Research.FirstDescent.Batch002
3+
import Collatz.Research.FirstDescent.Batch003
4+
import Collatz.Research.FirstDescent.Batch004
5+
import Collatz.Research.FirstDescent.Batch005
6+
import Collatz.Research.FirstDescent.Batch006
7+
import Collatz.Research.FirstDescent.Batch007
8+
import Collatz.Research.FirstDescent.Batch008
9+
import Collatz.Research.FirstDescent.Batch009
10+
import Collatz.Research.FirstDescent.Batch010
11+
import Collatz.Research.FirstDescent.Batch011
12+
import Collatz.Research.FirstDescent.Batch012
13+
import Collatz.Research.FirstDescent.Batch013
14+
import Collatz.Research.FirstDescent.Batch014
15+
import Collatz.Research.FirstDescent.Batch015
16+
import Collatz.Research.FirstDescent.Batch016
17+
import Collatz.Research.FirstDescent.Batch017
18+
import Collatz.Research.FirstDescent.Batch018
19+
import Collatz.Research.FirstDescent.Batch019
20+
import Collatz.Research.FirstDescent.Batch020
21+
import Collatz.Research.FirstDescent.Batch021
22+
import Collatz.Research.FirstDescent.Batch022
23+
import Collatz.Research.FirstDescent.Batch023
24+
import Collatz.Research.FirstDescent.Batch024
25+
import Collatz.Research.FirstDescent.Batch025
26+
import Collatz.Research.FirstDescent.Batch026
27+
import Collatz.Research.FirstDescent.Batch027
28+
import Collatz.Research.FirstDescent.Batch028
29+
import Collatz.Research.FirstDescent.Batch029
30+
import Collatz.Research.FirstDescent.Batch030
31+
import Collatz.Research.FirstDescent.Batch031
32+
import Collatz.Research.FirstDescent.Batch032
33+
import Collatz.Research.FirstDescent.Batch033
34+
import Collatz.Research.FirstDescent.Batch034
35+
import Collatz.Research.FirstDescent.Batch035
36+
import Collatz.Research.FirstDescent.Batch036
37+
import Collatz.Research.FirstDescent.Batch037
38+
import Collatz.Research.FirstDescent.Batch038
39+
import Collatz.Research.FirstDescent.Batch039
40+
import Collatz.Research.FirstDescent.Batch040
41+
import Collatz.Research.FirstDescent.Batch041
42+
import Collatz.Research.FirstDescent.Batch042
43+
import Collatz.Research.FirstDescent.Batch043
44+
import Collatz.Research.FirstDescent.Batch044
45+
import Collatz.Research.FirstDescent.Batch045
46+
import Collatz.Research.FirstDescent.Batch046
47+
import Collatz.Research.FirstDescent.Batch047
48+
import Collatz.Research.FirstDescent.Batch048
49+
import Collatz.Research.FirstDescent.Batch049
50+
import Collatz.Research.FirstDescent.Batch050
51+
import Collatz.Research.FirstDescent.Batch051
52+
import Collatz.Research.FirstDescent.Batch052
53+
import Collatz.Research.FirstDescent.Batch053
54+
import Collatz.Research.FirstDescent.Batch054
55+
import Collatz.Research.FirstDescent.Batch055
56+
import Collatz.Research.FirstDescent.Batch056
57+
import Collatz.Research.FirstDescent.Batch057
58+
import Collatz.Research.FirstDescent.Batch058
59+
import Collatz.Research.FirstDescent.Batch059
60+
import Collatz.Research.FirstDescent.Batch060
61+
import Collatz.Research.FirstDescent.Batch061
62+
import Collatz.Research.FirstDescent.Batch062
63+
import Collatz.Research.FirstDescent.Batch063
64+
import Collatz.Research.FirstDescent.Batch064
65+
import Collatz.Research.FirstDescent.Batch065
66+
import Collatz.Research.FirstDescent.Batch066
67+
import Collatz.Research.FirstDescent.Batch067
68+
import Collatz.Research.FirstDescent.Batch068
69+
import Collatz.Research.FirstDescent.Batch069
70+
import Collatz.Research.FirstDescent.Batch070
71+
import Collatz.Research.FirstDescent.Batch071
72+
import Collatz.Research.FirstDescent.Batch072
73+
import Collatz.Research.FirstDescent.Batch073
74+
import Collatz.Research.FirstDescent.Batch074
75+
import Collatz.Research.FirstDescent.Batch075
76+
import Collatz.Research.FirstDescent.Batch076
77+
import Collatz.Research.FirstDescent.Batch077
78+
import Collatz.Research.FirstDescent.Batch078
79+
import Collatz.Research.FirstDescent.Batch079
80+
import Collatz.Research.FirstDescent.Batch080
81+
import Collatz.Research.FirstDescent.Batch081
82+
import Collatz.Research.FirstDescent.Batch082
83+
import Collatz.Research.FirstDescent.Batch083
84+
import Collatz.Research.FirstDescent.Batch084
85+
import Collatz.Research.FirstDescent.Batch085
86+
import Collatz.Research.FirstDescent.Batch086
87+
import Collatz.Research.FirstDescent.Batch087
88+
import Collatz.Research.FirstDescent.Batch088
89+
import Collatz.Research.FirstDescent.Batch089
90+
import Collatz.Research.FirstDescent.Batch090
91+
import Collatz.Research.FirstDescent.Batch091
92+
import Collatz.Research.FirstDescent.Batch092
93+
import Collatz.Research.FirstDescent.Batch093
94+
import Collatz.Research.FirstDescent.Batch094
95+
import Collatz.Research.FirstDescent.Batch095
96+
import Collatz.Research.FirstDescent.Batch096
97+
import Collatz.Research.FirstDescent.Batch097
98+
import Collatz.Research.FirstDescent.Batch098
99+
import Collatz.Research.FirstDescent.Batch099
100+
import Collatz.Research.FirstDescent.Batch100
101+
import Collatz.Research.FirstDescent.Batch101
102+
import Collatz.Research.FirstDescent.Batch102
103+
import Collatz.Research.FirstDescent.Batch103
104+
import Collatz.Research.FirstDescent.Batch104
105+
import Collatz.Research.FirstDescent.Batch105
106+
import Collatz.Research.FirstDescent.Batch106
107+
import Collatz.Research.FirstDescent.Batch107
108+
import Collatz.Research.FirstDescent.Batch108
109+
import Collatz.Research.FirstDescent.Batch109
110+
import Collatz.Research.FirstDescent.Batch110
111+
import Collatz.Research.FirstDescent.Batch111
112+
import Collatz.Research.FirstDescent.Batch112
113+
import Collatz.Research.FirstDescent.Batch113
114+
import Collatz.Research.FirstDescent.Batch114
115+
import Collatz.Research.FirstDescent.Batch115
116+
import Collatz.Research.FirstDescent.Batch116
117+
import Collatz.Research.FirstDescent.Batch117
118+
import Collatz.Research.FirstDescent.Batch118
119+
import Collatz.Research.FirstDescent.Batch119
120+
import Collatz.Research.FirstDescent.Batch120
121+
import Collatz.Research.FirstDescent.Batch121
122+
import Collatz.Research.FirstDescent.Batch122
123+
import Collatz.Research.FirstDescent.Batch123
124+
import Collatz.Research.FirstDescent.Batch124
125+
import Collatz.Research.FirstDescent.Batch125
126+
import Collatz.Research.FirstDescent.Batch126
127+
import Collatz.Research.FirstDescent.Batch127
128+
import Collatz.Research.FirstDescent.Batch128
129+
import Collatz.Research.FirstDescent.Batch129
130+
import Collatz.Research.FirstDescent.Batch130
131+
import Collatz.Research.FirstDescent.Batch131
132+
import Collatz.Research.FirstDescent.Batch132
133+
import Collatz.Research.FirstDescent.Batch133
134+
import Collatz.Research.FirstDescent.Batch134
135+
import Collatz.Research.FirstDescent.Batch135
136+
import Collatz.Research.FirstDescent.Batch136
137+
import Collatz.Research.FirstDescent.Batch137
138+
import Collatz.Research.FirstDescent.Batch138
139+
import Collatz.Research.FirstDescent.Batch139
140+
import Collatz.Research.FirstDescent.Batch140
141+
import Collatz.Research.FirstDescent.Batch141
142+
import Collatz.Research.FirstDescent.Batch142
143+
import Collatz.Research.FirstDescent.Batch143
144+
import Collatz.Research.FirstDescent.Batch144
145+
import Collatz.Research.FirstDescent.Batch145
146+
import Collatz.Research.FirstDescent.Batch146
147+
import Collatz.Research.FirstDescent.Batch147
148+
import Collatz.Research.FirstDescent.Batch148
149+
import Collatz.Research.FirstDescent.Batch149
150+
import Collatz.Research.FirstDescent.Batch150
151+
import Collatz.Research.FirstDescent.Batch151
152+
import Collatz.Research.FirstDescent.Batch152
153+
import Collatz.Research.FirstDescent.Batch153
154+
import Collatz.Research.FirstDescent.Batch154
155+
import Collatz.Research.FirstDescent.Batch155
156+
import Collatz.Research.FirstDescent.Batch156
157+
import Collatz.Research.FirstDescent.Batch157
158+
import Collatz.Research.FirstDescent.Batch158
159+
import Collatz.Research.FirstDescent.Batch159
160+
import Collatz.Research.FirstDescent.Batch160
161+
import Collatz.Research.FirstDescent.Batch161
162+
import Collatz.Research.FirstDescent.Batch162
163+
import Collatz.Research.FirstDescent.Batch163
164+
import Collatz.Research.FirstDescent.Batch164
165+
import Collatz.Research.FirstDescent.Batch165
166+
import Collatz.Research.FirstDescent.Batch166
167+
import Collatz.Research.FirstDescent.Batch167
168+
import Collatz.Research.FirstDescent.Batch168
169+
import Collatz.Research.FirstDescent.Batch169
170+
import Collatz.Research.FirstDescent.Batch170
171+
import Collatz.Research.FirstDescent.Batch171
172+
import Collatz.Research.FirstDescent.Batch172
173+
import Collatz.Research.FirstDescent.Batch173
174+
import Collatz.Research.FirstDescent.Batch174
175+
import Collatz.Research.FirstDescent.Batch175
176+
import Collatz.Research.FirstDescent.Batch176
177+
import Collatz.Research.FirstDescent.Batch177
178+
import Collatz.Research.FirstDescent.Batch178
179+
import Collatz.Research.FirstDescent.Batch179
180+
import Collatz.Research.FirstDescent.Batch180
181+
import Collatz.Research.FirstDescent.Batch181
182+
import Collatz.Research.FirstDescent.Batch182
183+
import Collatz.Research.FirstDescent.Batch183
184+
import Collatz.Research.FirstDescent.Batch184
185+
import Collatz.Research.FirstDescent.Batch185
186+
import Collatz.Research.FirstDescent.Batch186
187+
import Collatz.Research.FirstDescent.Batch187
188+
import Collatz.Research.FirstDescent.Batch188
189+
import Collatz.Research.FirstDescent.Batch189
190+
import Collatz.Research.FirstDescent.Batch190
191+
import Collatz.Research.FirstDescent.Batch191
192+
import Collatz.Research.FirstDescent.Batch192
193+
import Collatz.Research.FirstDescent.Batch193
194+
import Collatz.Research.FirstDescent.Batch194
195+
import Collatz.Research.FirstDescent.Batch195
196+
import Collatz.Research.FirstDescent.Batch196
197+
import Collatz.Research.FirstDescent.Batch197
198+
import Collatz.Research.FirstDescent.Batch198
199+
import Collatz.Research.FirstDescent.Batch199
200+
import Collatz.Research.FirstDescent.Batch200
201+
import Collatz.Research.FirstDescent.Batch201
202+
import Collatz.Research.FirstDescent.Batch202
203+
import Collatz.Research.FirstDescent.Batch203
204+
import Collatz.Research.FirstDescent.Batch204
205+
import Collatz.Research.FirstDescent.Batch205
206+
import Collatz.Research.FirstDescent.Batch206
207+
import Collatz.Research.FirstDescent.Batch207
208+
import Collatz.Research.FirstDescent.Batch208
209+
import Collatz.Research.FirstDescent.Batch209
210+
import Collatz.Research.FirstDescent.Batch210
211+
import Collatz.Research.FirstDescent.Batch211
212+
import Collatz.Research.FirstDescent.Batch212
213+
import Collatz.Research.FirstDescent.Batch213
214+
import Collatz.Research.FirstDescent.Batch214
215+
import Collatz.Research.FirstDescent.Batch215
216+
import Collatz.Research.FirstDescent.Batch216
217+
import Collatz.Research.FirstDescent.Batch217
218+
import Collatz.Research.FirstDescent.Batch218
219+
import Collatz.Research.FirstDescent.Batch219
220+
import Collatz.Research.FirstDescent.Batch220
221+
import Collatz.Research.FirstDescent.Batch221
222+
import Collatz.Research.FirstDescent.Batch222
223+
import Collatz.Research.FirstDescent.Batch223
224+
import Collatz.Research.FirstDescent.Batch224
225+
import Collatz.Research.FirstDescent.Batch225
226+
import Collatz.Research.FirstDescent.Batch226
227+
import Collatz.Research.FirstDescent.Batch227
228+
import Collatz.Research.FirstDescent.Batch228
229+
import Collatz.Research.FirstDescent.Batch229
230+
import Collatz.Research.FirstDescent.Batch230
231+
import Collatz.Research.FirstDescent.Batch231
232+
import Collatz.Research.FirstDescent.Batch232
233+
import Collatz.Research.FirstDescent.Batch233
234+
import Collatz.Research.FirstDescent.Batch234
235+
import Collatz.Research.FirstDescent.Batch235
236+
import Collatz.Research.FirstDescent.Batch236
237+
import Collatz.Research.FirstDescent.Batch237
238+
import Collatz.Research.FirstDescent.Batch238
239+
import Collatz.Research.FirstDescent.Batch239
240+
import Collatz.Research.FirstDescent.Batch240
241+
import Collatz.Research.FirstDescent.Batch241
242+
import Collatz.Research.FirstDescent.Batch242
243+
import Collatz.Research.FirstDescent.Batch243
244+
import Collatz.Research.FirstDescent.Batch244
245+
import Collatz.Research.FirstDescent.Batch245
246+
import Collatz.Research.FirstDescent.Batch246
247+
import Collatz.Research.FirstDescent.Batch247
248+
import Collatz.Research.FirstDescent.Batch248
249+
import Collatz.Research.FirstDescent.Batch249
250+
import Collatz.Research.FirstDescent.Batch250
251+
import Collatz.Research.FirstDescent.Batch251
252+
import Collatz.Research.FirstDescent.Batch252
253+
import Collatz.Research.FirstDescent.Batch253
254+
import Collatz.Research.FirstDescent.Batch254
255+
import Collatz.Research.FirstDescent.Batch255
256+
import Collatz.Research.FirstDescent.Batch256
257+
import Collatz.Research.FirstDescent.Batch257
258+
import Collatz.Research.FirstDescent.Batch258
259+
import Collatz.Research.FirstDescent.Batch259
260+
import Collatz.Research.FirstDescent.Batch260
261+
import Collatz.Research.FirstDescent.Batch261
262+
import Collatz.Research.FirstDescent.Batch262
263+
import Collatz.Research.FirstDescent.Batch263
264+
import Collatz.Research.FirstDescent.Batch264
265+
import Collatz.Research.FirstDescent.Batch265
266+
import Collatz.Research.FirstDescent.Batch266
267+
import Collatz.Research.FirstDescent.Batch267
268+
import Collatz.Research.FirstDescent.Batch268
269+
import Collatz.Research.FirstDescent.Batch269
270+
import Collatz.Research.FirstDescent.Batch270
271+
import Collatz.Research.FirstDescent.Batch271
272+
import Collatz.Research.FirstDescent.Batch272
273+
import Collatz.Research.FirstDescent.Batch273
274+
import Collatz.Research.FirstDescent.Batch274
275+
import Collatz.Research.FirstDescent.Batch275
276+
import Collatz.Research.FirstDescent.Batch276
277+
import Collatz.Research.FirstDescent.Batch277
278+
import Collatz.Research.FirstDescent.Batch278
279+
import Collatz.Research.FirstDescent.Batch279
280+
import Collatz.Research.FirstDescent.Batch280
281+
import Collatz.Research.FirstDescent.Batch281
282+
import Collatz.Research.FirstDescent.Batch282
283+
import Collatz.Research.FirstDescent.Batch283
284+
import Collatz.Research.FirstDescent.Batch284
285+
import Collatz.Research.FirstDescent.Batch285
286+
import Collatz.Research.FirstDescent.Batch286
287+
import Collatz.Research.FirstDescent.Batch287
288+
import Collatz.Research.FirstDescent.Batch288
289+
import Collatz.Research.FirstDescent.Batch289
290+
import Collatz.Research.FirstDescent.Batch290
291+
import Collatz.Research.FirstDescent.Batch291
292+
import Collatz.Research.FirstDescent.Batch292
293+
import Collatz.Research.FirstDescent.Batch293
294+
import Collatz.Research.FirstDescent.Batch294
295+
import Collatz.Research.FirstDescent.Batch295
296+
import Collatz.Research.FirstDescent.Batch296
297+
import Collatz.Research.FirstDescent.Batch297
298+
import Collatz.Research.FirstDescent.Batch298
299+
import Collatz.Research.FirstDescent.Batch299
300+
import Collatz.Research.FirstDescent.Batch300

‎Collatz/Research/FirstDescent/CrossingGaps.lean‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
import Collatz.Research.DescentAtlas.Core
2+
3+
/-! Arithmetic gaps explain absent coefficient first-crossing times in the census.
4+
These results exclude a coefficient crossing at these horizons, not eventual
5+
integer descent. -/
6+
namespace Collatz.Research.FirstDescent.CrossingGaps
7+
8+
/-- If consecutive powers of three straddle a binary interval, no power of
9+
three lies in that interval. This applies uniformly to every odd-step count. -/
10+
theorem no_power_between {lo hi A : Nat}
11+
(hl : 3 ^ A < lo) (hh : hi ≤ 3 ^ (A + 1)) :
12+
∀ a : Nat, ¬ (lo ≤ 3 ^ a ∧ 3 ^ a < hi) := by
13+
intro a h
14+
by_cases ha : a ≤ A
15+
· have hp : 3 ^ a ≤ 3 ^ A := Nat.pow_le_pow_right (by decide) ha
16+
omega
17+
· have hp : 3 ^ (A + 1) ≤ 3 ^ a := Nat.pow_le_pow_right (by decide) (by omega)
18+
omega
19+
20+
/-- No coefficient first crossing can use the binary interval at time 3. -/
21+
theorem gap_3 : ∀ a : Nat, ¬ (2 ^ 2 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 3) := by
22+
exact no_power_between (A := 1) (by decide) (by decide)
23+
24+
/-- No coefficient first crossing can use the binary interval at time 6. -/
25+
theorem gap_6 : ∀ a : Nat, ¬ (2 ^ 5 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 6) := by
26+
exact no_power_between (A := 3) (by decide) (by decide)
27+
28+
/-- No coefficient first crossing can use the binary interval at time 9. -/
29+
theorem gap_9 : ∀ a : Nat, ¬ (2 ^ 8 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 9) := by
30+
exact no_power_between (A := 5) (by decide) (by decide)
31+
32+
/-- No coefficient first crossing can use the binary interval at time 11. -/
33+
theorem gap_11 : ∀ a : Nat, ¬ (2 ^ 10 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 11) := by
34+
exact no_power_between (A := 6) (by decide) (by decide)
35+
36+
/-- No coefficient first crossing can use the binary interval at time 14. -/
37+
theorem gap_14 : ∀ a : Nat, ¬ (2 ^ 13 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 14) := by
38+
exact no_power_between (A := 8) (by decide) (by decide)
39+
40+
/-- No coefficient first crossing can use the binary interval at time 17. -/
41+
theorem gap_17 : ∀ a : Nat, ¬ (2 ^ 16 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 17) := by
42+
exact no_power_between (A := 10) (by decide) (by decide)
43+
44+
/-- No coefficient first crossing can use the binary interval at time 19. -/
45+
theorem gap_19 : ∀ a : Nat, ¬ (2 ^ 18 ≤ 3 ^ a ∧ 3 ^ a < 2 ^ 19) := by
46+
exact no_power_between (A := 11) (by decide) (by decide)
47+
48+
end Collatz.Research.FirstDescent.CrossingGaps

0 commit comments

Comments
 (0)