"""Exact algebraic boundary scalar checks, with sqrt(1081) rational enclosure.
The analytic two-background source is not proved by this scalar computation.
"""
from pathlib import Path
import importlib.util,json,hashlib
import sympy as sy
from fractions import Fraction as F
from math import gcd,lcm
spec=importlib.util.spec_from_file_location('price_base',Path(__file__).with_name('certify_complete.py'))
m=importlib.util.module_from_spec(spec);spec.loader.exec_module(m)
q=sy.Rational;d,x=m.d,m.x;z=sy.sqrt(1081)
lo=q(3287856444554719302046,10**20);hi=q(3287856444554719302047,10**20)
assert lo**2<1081<hi**2
B2=(777-z)/852;b2=-q(11,71)+595*z/76751;d2=(61-z)/66
B=sy.symbols('boundary');ell=q(11,3)-4*B;h=(1+b2+3*ell)/2;ly=(1+b2-ell)/2;lx=(1-b2-ell)/2;T=2*ly-h;C0=-q(1,4)+b2/6+5*ell/4
p=m.p;theta0=m.theta0;Rd=m.Rd;Rs=m.Rs;md=m.md;rd=m.rd;td=m.td;Fd=m.Fd;J=m.J;JN=m.JN
E=lambda R:C0+d/2+d*x*(ell+(h/2-ly)/p)-3*h*(1-R)/4
S=lambda R:(3*R+1)/4+theta0/2-q(17,50)
N=lambda R:(3*R+1)/4-theta0/2
Dsh=lambda R:R+(q(1,2)-theta0)*q(3,40)-N(R)
GN=d*x*JN*T/10;GL=theta0*(q(7,10)*h-ly);GR=(d/2-theta0)*(ly-q(53,100)*h)
g=sy.cancel(GN-E(Rd),extension=z)
explicit=q(1,4)-b2/6-5*ell/4-d/2-d*x*ell+3*h*(1-Rd)/4+d*x*T/4
assert sy.simplify(g-explicit)==0
g0=sy.cancel(g.subs(B,B2),extension=z)
factor=(q(178,213)-q(5179,460506)*z)/(5-4*d)*(d-d2)**2
assert sy.simplify(g0.subs(x,q(1,2))-factor)==0
deriv=(-26*d**2*x**2+14*d**2*x+5*d*x-25*d+25)/(5-2*d-4*d*x)
assert sy.simplify(sy.diff(g,B)-deriv)==0

def lower(c):
 c=sy.expand(sy.radsimp(c));cc=sy.expand(c.xreplace({z:-z}));a=sy.simplify((c+cc)/2);b=sy.simplify((c-cc)/(2*z))
 assert a.is_Rational and b.is_Rational,(c,a,b)
 return a+b*(lo if b>=0 else hi)
def coefficients(poly):
 terms={ij:m.frac(lower(c)) for ij,c in sy.Poly(poly,d,x).terms()};den=lcm(*(v.denominator for v in terms.values()))
 terms={ij:int(v*den) for ij,v in terms.items()};gg=gcd(*(abs(v) for v in terms.values())) or 1
 return {ij:F(v//gg) for ij,v in terms.items() if v}
cert=[]
def positive(name,expr,box=m.Dmain):
 expr=expr.subs(B,B2);num,den=sy.fraction(sy.cancel(expr,extension=z));pt={d:q((box[0]+box[1])/2),x:q((box[2]+box[3])/2)}
 if float(den.subs(pt))<0:num,den=-num,-den
 rec={'name':name,'box':[str(v) for v in box]}
 for part,poly in [('numerator',num),('denominator',den)]:
  c=coefficients(poly);tree=m.prove(c,box)
  rec[part]={'coefficients':[[i,j,str(v)] for (i,j),v in sorted(c.items())],'tree':tree,'leaves':m.leaves(tree)}
 cert.append(rec)
for name,expr in [
 ('left numerator gain>1e-8',GL-E(Rd)-q(1,10**8)),('right numerator gain>1e-8',GR-E(Rd)-q(1,10**8)),
 ('main reference slope>1/5',S(Rd)-q(1,5)),('main reference slope<1',1-S(Rd)),('main reference exponent<1/250',q(1,250)-E(Rd)),
 ('main reference stock',(p-2*d*x)*m.stock-Rd),('short-source saving>1e-5',-E(Rd)-h*Dsh(Rd)-q(1,10**5)),
 ('short-source slope positive',S(Rd)+Dsh(Rd)),('short-source slope<2',2-S(Rd)-Dsh(Rd)),
 ('detector md>7/20',md-q(7,20)),('detector md<49/100',q(49,100)-md),('detector rd>3/5',rd-q(3,5)),('detector rd<1',1-rd),
 ('detector td>1',td-1),('detector td<3/2',q(3,2)-td),('detector upper m endpoint stronger',q(49,50)+x/50-Fd),('numerator saving bound',q(1,50)-d*x*JN*q(2,5)/10)
]:positive(name,expr)
for name,expr in [('old denominator positive',J),('old reference slope positive',S(Rs)),('old reference slope<1',1-S(Rs)),('old reference stock',(p-2*d*x)*m.stock-Rs)]:positive(name,expr,m.Omega)
for i,box in enumerate(m.comps):positive('complement reference saving>1e-5 '+str(i),-E(Rs)-q(1,10**5),box)
D0=(F(2,5),F(23,50),F(6,25),F(1,2));Dminus=(F(11,50),F(2,5),F(6,25),F(1,2));Dplus=(F(23,50),F(13,20),F(6,25),F(1,2))
trans=sy.cancel((g0-g0.subs(x,q(1,2)))/(q(1,2)-x),extension=z)
positive('contact edge coefficient>.113', (q(178,213)-q(5179,460506)*z)/(5-4*d)-q(113,1000))
positive('transverse contact gain>.009',trans-q(9,1000),D0)
positive('left noncontact gain>7e-5',g0-q(7,10**5),Dminus)
positive('right noncontact gain>7e-5',g0-q(7,10**5),Dplus)
positive('boundary derivative>2.37',deriv-q(237,100))
m0=1-ly/h;Qsm=ell*(q(1,2)+2*ell/h)-11*h/54
cs={
'b':b2,'ell>1/6':ell-q(1,6),'ell<1/5':q(1,5)-ell,'lx>ell':lx-ell,'Gram':ly-ell-11*b2/6,'p1 ell>3/4':p*ell-q(3,4),
'T':T,'ly<1/2':q(1,2)-ly,'principal B>.87':B-q(87,100),'stock top buffered':ell/(h+q(1,10**9))-m.stock,
'shortened stock<2/9':q(2,9)-ell/(h-q(1,40)),'m0>.30':m0-q(3,10),'m0<.47':q(47,100)-m0,'ly/h>.57':ly/h-q(57,100),'ly/h<.59':q(59,100)-ly/h,
'small amplitude coefficient':-Qsm,'small amplitude margin':-q(1,250)-C0-(1-h)/16,'floor margin':-q(1,1000)-C0-(q(1,2)+3*ell/2)/50,
'small rows margin':-q(1,20)-13*h/75+ly/2-q(1,50),'principal h/600':h/600,'principal ly/20':ly/20,
'reference theta0<.073':q(73,1000)-q(13,40)/p,'scale slope>.1':q(1,5)-q(73,1000)*q(37,40)-q(1,50)-q(1,10)}
constants={k:lower(sy.cancel(v.subs(B,B2),extension=z)) for k,v in cs.items()}
assert all(v>0 for v in constants.values())
out={'status':'PASS_EXACT_ALGEBRAIC_SCALAR_ONLY_WITH_TWO_BACKGROUND_MOMENT_GRANTED','theta_exact':'(777-sqrt(1081))/852',
'b_exact':'-11/71+595*sqrt(1081)/76751','sqrt_enclosure':[str(lo),str(hi)],'contact_factorization_verified_symbolically':True,'boundary_derivative_identity_verified_symbolically':True,
'certificates':cert,'positive_constants':{k:str(v) for k,v in constants.items()},
'coefficient_enclosure_scope':'Each a+b sqrt1081 coefficient is lowered using the exact rational enclosure. All monomials delta^i x^j are nonnegative on the positive rectangles.',
'complete_analytic_endpoint_proved_by_script':False,'Lean_endpoint':False,'tracker_admission':False}
path=Path(__file__).with_name('contact-certificate.json');path.write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps({'status':out['status'],'conditions':len(cert),'leaves':sum(z[k]['leaves'] for z in cert for k in ['numerator','denominator']),'constants':len(constants),'sha256':hashlib.sha256(path.read_bytes()).hexdigest()}))