"""Exact arithmetic diagnostics for main.tex, using Python's standard library.

Run: python3 verify.py
This verifies identities and sampled finite dual profiles. It is not a formal
proof checker and is not a replacement for the all-n mathematical argument.
Run verify_degree_transport.py separately for exhaustive small DFA checks.
"""
from fractions import Fraction as Q
from random import Random
from pathlib import Path
import json

beta=Q(25,129); gamma=Q(125,258); mu=Q(125,16641)
objective=Q(15625,1597536); alpha=Q(8257,49923)
gain=mu/25; coefficient=Q(8242,49923)

def F(x):
    return 5*mu*x/4-x**3/12+gamma**3/12-mu*gamma/4

assert mu==beta**2/5==gamma*(Q(1,2)-gamma)
assert F(beta)==objective
assert Q(7,48)+2*objective==alpha
assert alpha-gain==coefficient
assert gain==Q(5,16641)
assert Q(99,40)/50+Q(81,40*400)==Q(873,16000)
assert Q(1,18)-Q(873,16000)==Q(143,144000)>0
assert Q(9,20)*(1-Q(9,20))/(1-2*Q(9,20))==Q(99,40)
assert Q(9,20)**2/(1-2*Q(9,20))==Q(81,40)
assert Q(1,3)-Q(3,10)>0

integral=Q(3,2)*(Q(9,20)-Q(1,3))**2
cap_gain=(1-9*mu)*integral/10
assert cap_gain==Q(21119,11094000)>gain
outer_gains={
    'small_rho':2*objective-beta/16,
    'large_rho':2*(objective-F(Q(1,3))),
    'PF_tail':alpha-(1-gamma**3)/6,
}
assert outer_gains['small_rho']==Q(2975,399384)
assert outer_gains['large_rho']==Q(186,79507)
assert outer_gains['PF_tail']==Q(1822061,103041072)
assert all(x>gain for x in outer_gains.values())
for x in (beta/2,beta,Q(1,3),gamma):
    assert objective-F(x)==(x-beta)**2*(x+2*beta)/12

rng=Random(20261024)
checked=0
for n in (64,127,128,255,256,511,512,1024,2048):
    m=n//2; g=gamma.numerator*n//gamma.denominator
    mn=Q(g*(m-g))
    lo=(beta.numerator*n+2*beta.denominator-1)//(2*beta.denominator)
    hi=n//3
    for rho in sorted({lo,(lo+hi)//2,hi}):
        b=[Q(0)]*(m+1)
        for r in range(rho,m):
            b[r]=mn/Q(r*(r+1)) if r<g else Q(1)
            assert 0<=b[r]<=1
        suffix=[Q(0)]*(m+1)
        for r in range(m-1,rho-1,-1):suffix[r]=suffix[r+1]+b[r]
        for i in range(1,(n+1)//2+1):
            B=i*suffix[max(rho,i)] if i<m else Q(0)
            assert B<=mn*min(Q(1),Q(i,rho))
            if i<rho:assert B==mn*i/rho
            elif i<=g:assert B==mn
        dual=mn*rho+sum((1-b[r])*Q(r*r,4) for r in range(rho,m))
        expanded=mn*Q(5*rho-g,4)+sum(Q(r*r,4) for r in range(rho,g))
        expanded+=mn*sum(Q(1,r+1) for r in range(rho,g))/4
        assert dual==expanded
        assert abs(mn-mu*n*n)<=n+1
        for repeat in range(8):
            d=rng.randrange(rho+1)
            gaps=[0]*d
            if d:
                for _ in range(rng.randrange(n)):
                    gaps[rng.randrange(d)]+=1
            gaps.extend(rng.randrange(n+1) for _ in range(rho-d))
            s=[0]*((n+1)//2+1)
            for x in gaps:
                if x:s[(x+1)//2]+=1
            P=rho-sum(min(Q(1),Q(i,rho))*count for i,count in enumerate(s))
            assert P>=0
            assert P>=d-Q(sum(gaps[:d])+d,2*rho)
            G=[0]*len(s)
            for i in range(1,len(s)):G[i]=G[i-1]+i*s[i]
            z={r:min(Q(r*r,4),G[min(r,len(G)-1)]) for r in range(rho,m)}
            caps=sum((1-b[r])*(Q(r*r,4)-z[r]) for r in range(rho,m))
            assert sum(z.values())<=dual-mn*P-caps
            checked+=1

out={
    'status':'all exact rational assertions passed',
    'scope':'identities, branch margins, sampled finite dual and cheap-prefix profiles; not a formal proof checker',
    'profiles_checked':checked,
    'old_coefficient':str(alpha),
    'new_coefficient':str(coefficient),
    'new_coefficient_decimal':float(coefficient),
    'gain':str(gain),'gain_decimal':float(gain),
    'relative_coefficient_reduction_percent':float(100*gain/alpha),
    'cap_gain':str(cap_gain),
    'outer_gains':{k:str(v) for k,v in outer_gains.items()},
    'original_certificate_date':'2026-10-24',
    'verification_date':'2026-11-05',
}
print(json.dumps(out,indent=2))
Path(__file__).with_name('verification.json').write_text(json.dumps(out,indent=2)+'\n')