"""Fresh scalar certificates for the paper's fixed reference source.

These reproduce finite inequalities, not the general probability theorems or
Lean build. Directed integration follows manuscript Appendix D/check_paper.py.
"""
from fractions import Fraction as F
from math import factorial, prod, floor, ceil, log
from decimal import Decimal as D, localcontext, ROUND_FLOOR, ROUND_CEILING
from scipy.special import digamma, gammaincc, gammainc, gammaln, kv
from scipy.optimize import brentq
import numpy as np
from amplification import exp_negative


def timing_dual_certificate():
    q=[F(5,500),F(404,500),F(603,500),F(602,500),F(401,500)]
    def c(n,i):
        return F(0) if i<n else prod(q[n:])/q[i]/prod(q[j]-q[i] for j in range(n,5) if j!=i)
    ep=exp_negative(F(4));coef=[]
    for i in [0,4,1,3,2]:
        B=sum(F(4)**n/factorial(n)*c(n,i) for n in range(5))
        vals=[q[i]*(e*B-5*c(0,i)) for e in ep];scale=10**12
        coef.append((F(floor(min(vals)*scale),scale),F(ceil(max(vals)*scale),scale)))
    def params(side):
        z=[c[side] for c in coef];return -z[0],z[1],-z[2],z[3],-z[4]
    def H(B,Dd,E,G,x):return B-Dd*x**3+x**201*(E-G*x)
    A,B,Dd,E,G=params(1);v=F(9901,10000)
    upper=v**396*H(B,Dd,E,G,v)-A
    assert min(Dd,G,396*B-399*Dd*v**3,597*E-598*G*v)>=0 and upper<0
    A,B,Dd,E,G=params(0);grid=list(map(F,['.992','.994','.996','.998','1']));cells=[]
    for l,u in zip(grid,grid[1:]):
        derivative=-3*Dd*l*l+201*u**200*(E-G*l)-G*l**201
        lower=l**396*H(B,Dd,E,G,u)-A
        assert min(Dd,G,E-G*u,H(B,Dd,E,G,u),lower)>0 and derivative<0
        cells.append(dict(left=l,right=u,derivative_upper=derivative,polynomial_lower=lower))
    # x=exp(-t/500): t>=5 gives x<.9901; t<=4 gives x>.992.
    assert exp_negative(F(1,100))[1]<v and exp_negative(F(1,125))[0]>grid[0]
    return dict(coefficients=coef,upper_polynomial_at_v=upper,cells=cells,
                conclusion='loaded hit density >=5 times blank density before 4; <= after 5; manuscript likelihood-ratio theorem connects the middle interval')