\subsection*{\texttt{verify\_all.py}}
\begin{lstlisting}[language=Python]
"""Recompute the certificates for the planar seven-distance bound."""
import sys,subprocess,json
from pathlib import Path
if not __debug__: raise RuntimeError("Run without -O: assertions are proof checks")
import sympy
print("Python",sys.version,"SymPy",sympy.__version__,flush=True)
steps=[
 "computational_strategy/twelve_core_patterns.py",
 "seventeen_attack/reconstruct_eleven.py",
 "core_realizations/audit_eleven.py",
 "core_realizations/verify_eleven_cyclic.py",
 "core_extensions/eleven_lattice_extensions.py",
 "verify_circle_extensions.py",
]
for name in steps:
 print("VERIFY",name,flush=True)
 subprocess.run([sys.executable,name],check=True)
subprocess.run([sys.executable,"algebraic_bound/certify_cycle13.py","--all-words"],check=True)
c=json.loads(Path("algebraic_bound/cycle13_allwords_certificate.json").read_text())
assert (c["words"],c["total_intervals"],c["max_depth"])==(8190,8459,3)
Q=lambda a,b:a*a+a*b+b*b
H=[(a,b) for a in range(-3,4) for b in range(-3,4) if Q(a,b) in (0,1,3)]
X=H+[(-2,0),(0,2),(2,-2)]
assert len(set(X))==16
from collections import Counter
counts=Counter(Q(a-c,b-d) for i,(a,b) in enumerate(X) for c,d in X[:i])
assert dict(counts)=={1:33,3:24,4:18,7:24,9:9,12:6,13:6}
print("PASS: all computational certificates for g_2(7)=16",flush=True)

\end{lstlisting}

\subsection*{\texttt{computational\_strategy/twelve\_lattice\_cores.json}}
\begin{lstlisting}
[
{"index":0,"points":[[0,0],[0,1],[0,2],[0,3],[1,-1],[1,0],[1,1],[1,2],[2,0],[2,1],[3,-1],[3,0]],"squared_distances":[1,3,4,7,9,13]},
{"index":1,"points":[[0,0],[0,1],[0,2],[0,3],[1,0],[1,1],[1,2],[2,-1],[2,0],[2,1],[2,2],[3,0]],"squared_distances":[1,3,4,7,9,12]},
{"index":2,"points":[[0,0],[0,1],[0,2],[0,3],[1,0],[1,1],[1,2],[2,0],[2,1],[3,-1],[3,0],[3,1]],"squared_distances":[1,3,4,7,9,13]},
{"index":3,"points":[[0,0],[0,1],[0,2],[1,-2],[1,-1],[1,0],[1,1],[2,-1],[2,0],[2,1],[3,-2],[3,-1]],"squared_distances":[1,3,4,7,9,13]},
{"index":4,"points":[[0,0],[0,1],[0,2],[1,-1],[1,0],[1,1],[1,2],[2,-1],[2,0],[2,1],[3,-1],[3,0]],"squared_distances":[1,3,4,7,9]},
{"index":5,"points":[[0,0],[0,1],[0,2],[1,-1],[1,0],[1,1],[2,-2],[2,-1],[2,0],[2,1],[3,-1],[3,0]],"squared_distances":[1,3,4,7,9,12]},
{"index":6,"points":[[0,0],[0,1],[0,2],[1,-1],[1,0],[1,1],[2,-1],[2,0],[2,1],[3,-2],[3,-1],[3,0]],"squared_distances":[1,3,4,7,9,13]},
{"index":7,"points":[[0,0],[0,2],[1,-2],[1,-1],[1,0],[1,1],[2,-1],[2,0],[2,1],[3,-2],[3,-1],[4,-1]],"squared_distances":[1,3,4,7,9,13]},
{"index":8,"points":[[0,0],[0,2],[1,0],[1,1],[2,-1],[2,0],[2,1],[3,-2],[3,-1],[3,0],[3,1],[4,-1]],"squared_distances":[1,3,4,7,9,13]},
{"index":9,"points":[[0,0],[1,-2],[1,-1],[1,0],[1,1],[2,-2],[2,-1],[2,0],[3,-3],[3,-2],[3,0],[4,-2]],"squared_distances":[1,3,4,7,9,12]},
{"index":10,"points":[[0,0],[1,-2],[1,-1],[1,0],[1,1],[2,-2],[2,0],[3,-3],[3,-2],[3,-1],[3,0],[4,-2]],"squared_distances":[1,3,4,7,9,12]}
]

\end{lstlisting}

\subsection*{\texttt{computational\_strategy/twelve\_core\_patterns.py}}
\begin{lstlisting}[language=Python]
import json
from collections import Counter
from itertools import combinations

rows=json.load(open('computational_strategy/twelve_lattice_cores.json'))
patterns=[]
for row in rows:
 pts=row['points']; D=row['squared_distances'];lookup={d:i+1 for i,d in enumerate(D)}
 M=[[0]*12 for _ in range(12)]
 for i in range(12):
  for j in range(i):
   a=pts[i][0]-pts[j][0];b=pts[i][1]-pts[j][1]
   M[i][j]=M[j][i]=lookup[a*a+a*b+b*b]
 patterns.append(dict(name='L'+str(row['index']),matrix=M,points=pts,palette=D))
for name,n,verts,center in [('R13minus1',13,list(range(12)),False),('R12',12,list(range(12)),False),('R12minus1_plusO',12,list(range(11)),True),('R11plusO',11,list(range(11)),True)]:
 M=[[0]*12 for _ in range(12)]
 for i in range(len(verts)):
  for j in range(i):
   delta=abs(verts[i]-verts[j]);M[i][j]=M[j][i]=min(delta,n-delta)
 if center:
  color=2 if n==12 else 6
  for i in range(11):M[i][11]=M[11][i]=color
 patterns.append(dict(name=name,matrix=M))

for pattern in patterns:
 M=pattern['matrix'];colorcounts=Counter(M[i][j] for i in range(12) for j in range(i))
 signature=tuple(sorted(colorcounts.values()))
 vertexsig=[]
 for i in range(12):
  vc=Counter(M[i][j] for j in range(12) if i!=j)
  vertexsig.append(tuple(sorted((colorcounts[c],vc[c]) for c in colorcounts)))
 invariant=(signature,tuple(sorted(vertexsig)))
 pattern['edge_count_signature']=signature
 pattern['vertex_signature']=sorted(vertexsig)
 print(pattern['name'],signature,'vertexsig distinct',len(set(vertexsig)))
# Invariants are unchanged by both vertex permutations and arbitrary color relabeling.
invariants=[(p['edge_count_signature'],tuple(p['vertex_signature'])) for p in patterns]
assert len(patterns)==15 and len(set(invariants))==15
assert all(len(set(p.get('palette',[])))<=6 for p in patterns)
print('Distinct simple invariants:',len(set(invariants)),'outof',len(patterns))
for i,j in combinations(range(len(patterns)),2):
 if invariants[i]==invariants[j]:print('Need fuller isomorphism check',patterns[i]['name'],patterns[j]['name'])
with open('computational_strategy/twelve_core_patterns.json','w') as f:json.dump(patterns,f,indent=2)

\end{lstlisting}

\subsection*{\texttt{seventeen\_attack/reconstruct\_eleven.py}}
\begin{lstlisting}[language=Python]
"""Reconstruct62pairwise inequivalent realized distance patterns on11points.
Only existence and distinctness are proved here. Completeness uses the published
Table9candidatecount; metricrealization rigidity is a separate calculation.
"""
import json
from collections import Counter
from pathlib import Path
if not __debug__:raise RuntimeError('Run without -O')
rows=json.loads(Path('computational_strategy/twelve_core_patterns.json').read_text())

def invariant(M):
    colors=set(sum(M,[]))-{0}
    ec=Counter(M[i][j] for i in range(len(M)) for j in range(i))
    # The unordered globalcolorfrequencies and unordered vertexcolorfrequencies
    # are preserved by arbitrary vertex and color relabeling.
    vs=[tuple(sorted((ec[c],sum(x==c for x in row)) for c in colors)) for row in M]
    return tuple(sorted(ec.values())),tuple(sorted(vs))

patterns={}
for row in rows:
    M0=row['matrix']
    if 'points' in row:
        pts=row['points'];palette=row['palette']
        for i in range(12):
            for j in range(i):
                a,b=pts[i][0]-pts[j][0],pts[i][1]-pts[j][1]
                assert a*a+a*b+b*b==palette[M0[i][j]-1]
    for removed in range(12):
        keep=[i for i in range(12) if i!=removed]
        M=[[M0[i][j] for j in keep] for i in keep]
        key=invariant(M)
        if key not in patterns:
            item=dict(name=row['name']+'minus'+str(removed),matrix=M,source=row['name'],deleted=removed)
            if 'points' in row:item['points']=[row['points'][i] for i in keep];item['source_palette']=row['palette']
            patterns[key]=item
assert len(patterns)==61
M=[[0]*11 for _ in range(11)]
for i in range(10):
    for j in range(i):M[i][j]=M[j][i]=min(i-j,10-i+j)
    M[i][10]=M[10][i]=6
assert invariant(M) not in patterns
patterns[invariant(M)]=dict(name='R10plusO',matrix=M)
assert len(patterns)==62
out=list(patterns.values())
assert sum('points' in r for r in out)==52
Path('seventeen_attack/eleven_patterns.json').write_text(json.dumps(out,indent=2))
print('PASS:62distinct realized coloredpatterns,52lattice and10circular')

\end{lstlisting}

\subsection*{\texttt{core\_realizations/audit\_eleven.py}}
\begin{lstlisting}[language=Python]
"""Fresh exact audit of all eleven-point pattern realizations.
Uses explicit 3x3 determinant formulas, not saved bases.
"""
import sympy as s,json,time
from itertools import combinations
from collections import Counter
from pathlib import Path
if not __debug__: raise RuntimeError('Run without -O')
rows=json.load(open('seventeen_attack/eleven_patterns.json'))
assert len(rows)==62 and sum('points' in r for r in rows)==52
assert sum('points' not in r for r in rows)==10
signatures=[]
for row in rows:
 M=row['matrix'];assert len(M)==11 and all(len(r)==11 for r in M)
 colors=set(sum(M,[]))-{0};assert len(colors)<=6
 assert all(M[i][j]==M[j][i] and (M[i][j]==0)==(i==j) for i in range(11) for j in range(11))
 ec=Counter(M[i][j] for i,j in combinations(range(11),2))
 signatures.append((tuple(sorted(ec.values())),tuple(sorted(tuple(sorted((ec[c],sum(x==c for x in r)) for c in colors)) for r in M))))
 if 'points' in row:
  pts=row['points'];palette=row['source_palette'];assert len(pts)==11 and len(set(map(tuple,pts)))==11
  for i,j in combinations(range(11),2):
   a,b=pts[i];c,d=pts[j]
   assert (a-c)**2+(a-c)*(b-d)+(b-d)**2==palette[M[i][j]-1]
assert len(set(signatures))==62
print('PASS 62 distinct patterns and 52 exact lattice realizations',flush=True)
outdir=Path('core_realizations/eleven');outdir.mkdir(exist_ok=True)
completed=0
for ix,row in enumerate(rows):
 name=row['name'];out=outdir/(name+'.json')
 M=row['matrix'];colors=sorted(set(sum(M,[]))-{0});k=len(colors)
 xs=s.symbols('x2:'+str(k+1));ds=dict(zip(colors,[s.Integer(1)]+list(xs)));ds[0]=s.Integer(0)
 G=[[ds[M[0][i+1]]+ds[M[0][j+1]]-ds[M[i+1][j+1]] for j in range(10)] for i in range(10)]
 polys=[]
 for i,j,l in combinations(range(10),3):
  a,b,c=G[i][i],G[j][j],G[l][l];d,e,f=G[i][j],G[i][l],G[j][l]
  polys.append(s.expand(a*b*c+2*d*e*f-a*f*f-b*e*e-c*d*d))
 ps=sorted(set(polys)-{0},key=str)
 start=time.time();print(ix+1,name,'BEGIN',len(ps),flush=True)
 gb=s.groebner(ps,*xs,order='grevlex')
 u=s.Symbol('u');sat=s.groebner([p.as_expr() for p in gb.polys]+[u*s.prod(xs)-1],u,*xs,order='lex')
 eliminated=[p.as_expr() for p in sat.polys if not p.as_expr().has(u)]
 output={'name':name,'variables':[str(x) for x in xs],'original_colors':colors,'saturated':[str(p) for p in eliminated]}
 out.write_text(json.dumps(output,indent=2))
 if 'points' in row:
  old=row['source_palette'];palette=[s.Rational(old[c-1],old[colors[0]-1]) for c in colors]
  target=[v-q for v,q in zip(xs,palette[1:])]
  if len(eliminated)!=len(target) or any(s.expand(p-q)!=0 for p,q in zip(eliminated,target)):
   raise RuntimeError(('NONLINEAR OR ALTERNATIVE LATTICE SOLUTIONS',name,eliminated))
  else:print('UNIQUE LATTICE',name,flush=True)
 completed+=1
 print(ix+1,name,'DONE',round(time.time()-start,2),flush=True)

assert completed==62
print('PASS all 62 fresh exact Gram-minor computations',flush=True)

\end{lstlisting}

\subsection*{\texttt{core\_realizations/verify\_eleven\_cyclic.py}}
\begin{lstlisting}[language=Python]
"""Exhaust all metric solutions of the ten circular eleven-point patterns."""
import sympy as s,json,math
from pathlib import Path
if not __debug__:raise RuntimeError('Run without -O')
z=s.Symbol('z')
rows=json.load(open('seventeen_attack/eleven_patterns.json'))
for row in rows:
 if 'points' in row:continue
 name=row['name'];n=int(name[1:3]);center=(n==10 or n==11 and name!='R11plusOminus11')
 phi=s.Poly(s.cyclotomic_poly(n,z),z,domain=s.QQ)
 def red(x):return s.rem(s.Poly(x,z,domain=s.QQ),phi).as_expr()
 def chord(k):return red(2-z**(k%n)-z**((-k)%n))
 d=json.loads((Path('core_realizations/eleven')/(name+'.json')).read_text())
 colors=d['original_colors'];xs=s.symbols(' '.join(d['variables']));polys=[s.Poly(s.sympify(p),*xs) for p in d['saturated']]
 assert colors[0]==1
 # Triangular equations ensure exactly one full distance assignment per final root.
 assert len(polys)==len(xs)
 t=xs[-1]
 for v,p in zip(xs[:-1],polys[:-1]):
  e=p.as_expr();assert e.free_symbols<=set([v,t]) and s.diff(e,v).is_Rational and s.diff(e,v)!=0
 assert polys[-1].as_expr().free_symbols=={t}
 # Reconstruct the actual retained polygon labels, with None for the center.
 if n==13: labels=list(range(12))
 elif n==12 and row.get('source')=='R12': labels=list(range(12))
 elif n==12: labels=list(range(11))+[None]
 elif n==11: labels=list(range(11))+[None]
 else: labels=list(range(10))+[None]
 if 'deleted' in row: labels.pop(row['deleted'])
 assert len(labels)==11
 js=[j for j in range(1,n//2+1) if math.gcd(j,n)==1];seen=[]
 for j in js:
  inv=s.invert(chord(j),phi.as_expr(),z)
  vals=[red(inv if center and c==6 else chord(c*j)*inv) for c in colors[1:]]
  # Every exhibited tuple realizes the original colored distance matrix.
  values={0:s.Integer(0),colors[0]:s.Integer(1)}
  values.update(zip(colors[1:],vals))
  for a in range(11):
   for b in range(a):
    raw=s.Integer(1) if labels[a] is None or labels[b] is None else chord((labels[a]-labels[b])*j)
    assert red(raw*inv-values[row['matrix'][a][b]])==0,(name,j,a,b)
  for p in polys:
   result=0
   for powers,coeff in p.terms():
    term=coeff
    for val,power in zip(vals,powers):term=red(term*red(val**power))
    result=red(result+term)
   assert result==0,(name,j,p,result)
  seen.append(vals[-1])
 assert len(set(seen))==len(js)
 assert s.degree(polys[-1].as_expr(),t)==len(js)
 print(name,': exactly',len(js),'solutions; all relabeled/scaled regular-polygon subsets',flush=True)
print('PASS all ten circular eleven-point metric classifications')

\end{lstlisting}

\subsection*{\texttt{core\_extensions/lattice\_diameter\_extensions.py}}
\begin{lstlisting}[language=Python]
#!/usr/bin/env python3
"""Exact exhaustive one-new-largest-distance extensions of ten twelve-point cores.
All coordinates are triangular lattice coordinates, but candidate coordinates
are arbitrary rational solutions obtained from distances to three nonextreme
anchors. A geometric proof guarantees these distances belong to the old palette.
"""
from fractions import Fraction as F
from itertools import combinations,product
import json
from pathlib import Path
if not __debug__: raise RuntimeError('Assertions required; run without -O.')
def Q(p):return p[0]*p[0]+p[0]*p[1]+p[1]*p[1]
def d(p,q):return Q((p[0]-q[0],p[1]-q[1]))
def cross(a,b,c):return(b[0]-a[0])*(c[1]-a[1])-(b[1]-a[1])*(c[0]-a[0])
def hull(P):
 H=[]
 for p in sorted(P):
  while len(H)>1 and cross(H[-2],H[-1],p)<=0:H.pop()
  H.append(p)
 L=len(H)
 for p in sorted(P,reverse=True)[1:]:
  while len(H)>L and cross(H[-2],H[-1],p)<=0:H.pop()
  H.append(p)
 return H[:-1]
def anchored(A,B,C,S):
 l1=2*(B[0]-A[0])+B[1]-A[1];m1=B[0]-A[0]+2*(B[1]-A[1])
 l2=2*(C[0]-A[0])+C[1]-A[1];m2=C[0]-A[0]+2*(C[1]-A[1])
 det=l1*m2-l2*m1;assert det
 out=set()
 for a,b,c in product(S,repeat=3):
  r1=Q(B)-Q(A)+a-b;r2=Q(C)-Q(A)+a-c
  p=(F(r1*m2-r2*m1,det),F(l1*r2-l2*r1,det))
  if d(p,A)==a:
   assert d(p,B)==b and d(p,C)==c
   out.add(p)
 return out
def clique(P,S):
 best=[]
 def go(picked,remaining):
  nonlocal best
  if len(picked)+len(remaining)<=len(best):return
  if len(picked)>len(best):best=picked
  while remaining:
   p=remaining.pop()
   go(picked+[p],[q for q in remaining if d(p,q) in S])
 go([],P[:]);return best
rows=json.loads(Path('computational_strategy/twelve_lattice_cores.json').read_text())
cert=[]
for row in rows:
 S=set(row['squared_distances'])
 if len(S)!=6:continue
 P=list(map(tuple,row['points']));H=hull(P);I=[p for p in P if p not in H]
 anchors=next(t for t in combinations(I,3) if cross(*t))
 C=anchored(*anchors,S)-set(P)
 C={p for p in C if all(d(p,a) in S for a in I)}
 new={p:{d(p,a) for a in P}-S for p in C}
 C=sorted(p for p in C if len(new[p])<=1 and all(t>max(S) for t in new[p]))
 ts={t for p in C for t in new[p]}|{d(p,q) for p,q in combinations(C,2) if d(p,q)>max(S)}
 # Include old-only extension case as an independent guard.
 cases=[]
 for t in [None]+sorted(ts):
  T=S if t is None else S|{t}
  V=[p for p in C if all(d(p,a) in T for a in P)]
  best=clique(V,T)
  cases.append(dict(T=str(t),vertices=[[str(x) for x in p] for p in V],max_added=len(best),witness=[[str(x) for x in p] for p in best]))
 maxn=12+max(c['max_added'] for c in cases)
 print(row['index'],'anchors',anchors,'candidates',len(C),'Ts',list(map(str,sorted(ts))),'max_total',maxn,flush=True)
 cert.append(dict(index=row['index'],palette=sorted(S),hull=H,nonextreme=I,anchors=anchors,cases=cases,max_total=maxn))
 assert maxn<=16
Path('core_extensions/lattice_diameter_extensions.json').write_text(json.dumps(cert,indent=2))
print('PASS: all ten six-distance lattice cores have at most sixteen points in a one-new-largest-distance extension.')

\end{lstlisting}

\subsection*{\texttt{core\_extensions/eleven\_lattice\_extensions.py}}
\begin{lstlisting}[language=Python]
#!/usr/bin/env python3
"""Exact largest-diameter extensions of the52 reconstructed eleven-point lattice cores.
Five-distance cores use exact quadratic circle intersections, not assumed rationality.
"""
from fractions import Fraction as F
from itertools import combinations,product
from pathlib import Path
import json
if not __debug__:raise RuntimeError('Assertions required')
exec(Path('core_extensions/lattice_diameter_extensions.py').read_text().split('rows=json.loads')[0])
# q=(ax+bx*sqrt(D),ay+by*sqrt(D)); D is zero or positive squarefree integer.
def sqrt_normalize(k):
 assert k>=0
 if not k:return F(0),0
 n=k.numerator*k.denominator;den=k.denominator;f=1;D=1;p=2
 while p*p<=n:
  e=0
  while n%p==0:e+=1;n//=p
  f*=p**(e//2)
  if e%2:D*=p
  p+=1
 if n>1:D*=n
 return F(f,den),D

def pq(x,y):return(F(x),F(0),F(y),F(0),0)
def qdist(q,p):
 ax,bx,ay,by,D=q;ax-=p[0];ay-=p[1]
 u=ax*ax+ax*ay+ay*ay+D*(bx*bx+bx*by+by*by)
 v=2*ax*bx+ax*by+ay*bx+2*ay*by
 return(u,v,D if v else 0)
def old(v,S):return v[1]==0 and v[0] in S
def pair_candidates(A,B,S):
 w=(B[0]-A[0],B[1]-A[1]);L=Q(w);out=set()
 for a,b in product(S,repeat=2):
  t=F(a-b+L,2*L);k=F(a-t*t*L,3*L)
  if k<0:continue
  f,D0=sqrt_normalize(k)
  for sig in [-1,1]:
   D=D0
   ax=F(A[0])+t*w[0];ay=F(A[1])+t*w[1]
   bx=sig*f*(-w[0]-2*w[1]);by=sig*f*(2*w[0]+w[1])
   if D==1:ax+=bx;ay+=by;bx=by=F(0);D=0
   q=(ax,bx,ay,by,D)
   assert qdist(q,A)==(F(a),F(0),0) and qdist(q,B)==(F(b),F(0),0)
   out.add(q)
 return out

def circumcenter(A,B,C):
 l1=2*(B[0]-A[0])+B[1]-A[1];m1=B[0]-A[0]+2*(B[1]-A[1])
 l2=2*(C[0]-A[0])+C[1]-A[1];m2=C[0]-A[0]+2*(C[1]-A[1]);det=l1*m2-l2*m1
 assert det
 r1=Q(B)-Q(A);r2=Q(C)-Q(A)
 return pq(F(r1*m2-r2*m1,det),F(l1*r2-l2*r1,det))

base={x['name']:x for x in json.loads(Path('computational_strategy/twelve_core_patterns.json').read_text())}
results=[]
for row in json.loads(Path('seventeen_attack/eleven_patterns.json').read_text()):
 if not row['name'].startswith('L'):continue
 P=[tuple(p) for i,p in enumerate(base[row['source']]['points']) if i!=row['deleted']]
 S={d(a,b) for a,b in combinations(P,2)};I=sorted(set(P)-set(hull(P)))
 assert len(P)==11 and len(S) in [5,6]
 label_to_distance={}
 for i,j in combinations(range(11),2):
  label=row['matrix'][i][j];value=d(P[i],P[j])
  assert label not in label_to_distance or label_to_distance[label]==value
  label_to_distance[label]=value
 assert len(set(label_to_distance.values()))==len(label_to_distance)==len(S)
 if len(S)==6:
  anchors=next(t for t in combinations(I,3) if cross(*t))
  C=anchored(*anchors,S)-set(P)
  C={p for p in C if all(d(p,a) in S for a in I)}
  new={p:{d(p,a) for a in P}-S for p in C}
  C=sorted(p for p in C if len(new[p])<=1 and all(t>max(S) for t in new[p]))
  ts={t for p in C for t in new[p]}|{d(p,q) for p,q in combinations(C,2) if d(p,q)>max(S)}
  cases=[]
  for t in [None]+sorted(ts):
   T=S if t is None else S|{t}
   V=[p for p in C if all(d(p,a) in T for a in P)]
   best=clique(V,T)
   cases.append(dict(extras=[str(t)],max_total=11+len(best),witness=[[str(x) for x in p] for p in best]))
 else:
  assert len(I)>=5
  C=set()
  for A,B in combinations(I,2):C|=pair_candidates(A,B,S)
  for t in combinations(I,3):
   if cross(*t):C.add(circumcenter(*t))
  C-={pq(*p) for p in P}
  C={q for q in C if len({v for p in I if not old(v:=qdist(q,p),S)})<=1 and len({v for p in P if not old(v:=qdist(q,p),S)})<=2}
  # Verify, rather than assume, all surviving candidates are rational.
  assert all(q[1]==q[3]==0 for q in C),(row['name'],'nonrational survivors',[q for q in C if q[1] or q[3]])
  C=sorted((q[0],q[2]) for q in C)
  values={d(q,p) for q in C for p in P}-S
  values|={d(a,b) for a,b in combinations(C,2)}-S
  cases=[]
  for a,b in combinations(sorted(values),2):
   if b<=max(S):continue
   T=S|{a,b}
   V=[q for q in C if all(d(q,p) in T for p in P) and all(d(q,p)!=b for p in I)]
   best=clique(V,T)
   cases.append(dict(extras=[str(a),str(b)],max_total=11+len(best),witness=[[str(x) for x in q] for q in best]))
  # Extensions with fewer than7distances haveatmost13points bypublishedtheorem.
  cases.append(dict(extras=['at most one'],max_total=13,witness=[]))
 maximum=max(c['max_total'] for c in cases)
 print(row['name'],'old',len(S),'interior',len(I),'candidates',len(C),'max',maximum,flush=True)
 results.append(dict(name=row['name'],points=P,palette=sorted(S),nonextreme=I,candidates=[[str(x) for x in p] for p in C],max_total=maximum,cases=cases))
 assert maximum<=16,(row['name'],maximum)
Path('core_extensions/eleven_lattice_extensions.json').write_text(json.dumps(results,indent=2))
print('PASS: all',len(results),'eleven-point lattice cores extend to at most16points.')

\end{lstlisting}

\subsection*{\texttt{verify\_circle\_extensions.py}}
\begin{lstlisting}[language=Python]
"""Exact axis certificates for all circular eleven-point core families."""
from fractions import Fraction as F
from itertools import combinations,permutations
from collections import Counter
if not __debug__:raise RuntimeError('Run without -O')
class Field:
 def __init__(self,mod):
  self.mod=tuple(map(F,mod));self.r=len(mod)-1
  self.zero=(F(0),)*self.r;self.one=self.scalar(1)
  self.u=(F(0),F(1))+(F(0),)*(self.r-2)
 def scalar(self,a):return(F(a),)+(F(0),)*(self.r-1)
 def add(self,a,b):return tuple(x+y for x,y in zip(a,b))
 def sub(self,a,b):return tuple(x-y for x,y in zip(a,b))
 def neg(self,a):return tuple(-x for x in a)
 def mul(self,a,b):
  c=[F(0)]*(2*self.r-1)
  for i,x in enumerate(a):
   for j,y in enumerate(b):c[i+j]+=x*y
  for i in range(len(c)-1,self.r-1,-1):
   for j in range(self.r):c[i-self.r+j]-=c[i]*self.mod[j]
  return tuple(c[:self.r])
 def inverse(self,a):
  assert a!=self.zero
  columns=[self.mul(a,tuple(F(i==j) for i in range(self.r))) for j in range(self.r)]
  M=[[columns[j][i] for j in range(self.r)]+[F(i==0)] for i in range(self.r)]
  for j in range(self.r):
   pivot=next(i for i in range(j,self.r) if M[i][j]);M[j],M[pivot]=M[pivot],M[j]
   d=M[j][j];M[j]=[x/d for x in M[j]]
   for i in range(self.r):
    if i!=j:
     d=M[i][j];M[i]=[x-d*y for x,y in zip(M[i],M[j])]
  result=tuple(M[i][-1] for i in range(self.r))
  assert self.mul(a,result)==self.one
  return result
# Coefficients of the monic minimal polynomial, constant term first.
cases=[(13,(-1,3,6,-4,-5,1,1)),(12,(1,0,-4,0,1)),
       (11,(1,3,-3,-4,1,1)),(10,(5,0,-5,0,1))]
expected={(13,'vertex'):{0:355,1:6,6:1},
 (12,'vertex'):{0:108,1:2,2:8,6:2},(12,'edge'):{0:86,3:6},
 (11,'vertex'):{0:156,1:5,5:1},
 (10,'vertex'):{0:110,1:2,2:4,3:4,5:2},(10,'edge'):{0:68,1:4}}
for n,mod in cases:
 K=Field(mod);period=n if n%2 else 2*n
 C=[K.scalar(2),K.u]
 for j in range(2,period+1):C.append(K.sub(K.mul(K.u,C[-1]),C[-2]))
 assert C[period]==K.scalar(2)
 old_indices=range(1,n//2+1) if n%2 else range(2,n+1,2)
 OLD={K.sub(K.scalar(2),C[j]) for j in old_indices}
 if n==10:OLD.add(K.one)
 axes=[('vertex',list(range(n//2+1)))] if n%2 else [
   ('vertex',list(range(0,n+1,2))),('edge',list(range(1,n,2)))]
 for axis,indices in axes:
  parameters=set()
  for j,k in combinations(indices,2):
   inv=K.inverse(K.sub(C[j],C[k]))
   for a,b in permutations(OLD,2):parameters.add(K.mul(K.sub(b,a),inv))
  assert K.zero not in parameters
  threshold=5 if n==13 or (n==10 and axis=='vertex') else (3 if n==11 else 4)
  histogram=Counter();survivors=set()
  for t in parameters:
   radii={K.sub(K.add(K.mul(t,t),K.one),K.mul(t,C[j])) for j in indices}
   assert len(radii)==len(indices)
   overlap=len(radii&OLD);histogram[overlap]+=1
   if overlap>=threshold:survivors.add(t)
  assert dict(histogram)==expected[n,axis]
  allowed=set() if axis=='edge' else ({K.one} if n%2 else {K.one,K.neg(K.one)})
  assert survivors==allowed
  print('PASS R'+str(n),axis,'parameters',len(parameters),'histogram',dict(sorted(histogram.items())))
print('PASS: all circular core families have only polygon vertices or center as possible points')

\end{lstlisting}

\subsection*{\texttt{algebraic\_bound/certify\_cycle13.py}}
\begin{lstlisting}[language=Python]
#!/usr/bin/env python3
"""Exact integer-arithmetic certificate: nonconstant binary-angle diameter C13 cannot close.
No external dependencies. Fixed-point intervals round every product/division outward.
"""
from fractions import Fraction
from math import factorial
from pathlib import Path
from functools import lru_cache
import json,time,sys
if not __debug__:
 raise RuntimeError("Run without -O: proof checks require assertions.")
N=13
S=10**50
assert 4**121*S < factorial(121)

def trim(a):
 while len(a)>1 and a[-1]==0:a.pop()
 return a

def idiv(a,b):
 a=a[:];q=[0]*max(1,len(a)-len(b)+1)
 for k in range(len(a)-len(b),-1,-1):
  assert b[-1]==1
  q[k]=a[k+len(b)-1]
  for j,x in enumerate(b):a[k+j]-=q[k]*x
 assert all(x==0 for x in a)
 return trim(q)
cyclo={}
for n in range(1,25):
 p=[-1]+[0]*(n-1)+[1]
 for d in range(1,n):
  if n%d==0:p=idiv(p,cyclo[d])
 cyclo[n]=p

def atan_bounds(inv, terms=100):
 p=Fraction(0)
 for k in range(terms):p+=Fraction((-1)**k,(2*k+1)*inv**(2*k+1))
 e=Fraction(1,(2*terms+1)*inv**(2*terms+1))
 return (p,p+e) if terms%2==0 else (p-e,p)
a,b=atan_bounds(5);c,d=atan_bounds(239)
pi_lo,pi_hi=16*a-4*d,16*b-4*c
PI=(pi_lo.numerator*S//pi_lo.denominator,-((-pi_hi.numerator*S)//pi_hi.denominator))
assert 3*S<PI[0]<=PI[1]<4*S

def add(a,b):return(a[0]+b[0],a[1]+b[1])
def neg(a):return(-a[1],-a[0])
def sub(a,b):return add(a,neg(b))
def mul(a,b):
 p=[x*y for x in a for y in b]
 return(min(p)//S,-((-max(p))//S))
def divi(a,n):return(a[0]//n,-((-a[1])//n))
def scale(a,n):return(a[0]*n,a[1]*n) if n>=0 else(a[1]*n,a[0]*n)

@lru_cache(None)
def trig_pi(num,den):
 # Both sine and cosine are enclosed by 61 Taylor terms at x in [0,pi].
 # Remainder <=4^121/121! <1e-120 < 1/S.
 x=divi(scale(PI,num),den);assert 0<=x[0]<=x[1]<=4*S
 xx=mul(x,x);st=x;ct=(S,S);sn=x;cs=ct
 for k in range(1,61):
  st=divi(mul(st,xx),(2*k)*(2*k+1))
  ct=divi(mul(ct,xx),(2*k-1)*(2*k))
  sn=add(sn,st if k%2==0 else neg(st))
  cs=add(cs,ct if k%2==0 else neg(ct))
 return((sn[0]-1,sn[1]+1),(cs[0]-1,cs[1]+1))

def cmul(a,b):
 return(sub(mul(a[0],b[0]),mul(a[1],b[1])),add(mul(a[0],b[1]),mul(a[1],b[0])))
def cadd(a,b):return(add(a[0],b[0]),add(a[1],b[1]))
def zero_excluded(a):return a[0][0]>0 or a[0][1]<0 or a[1][0]>0 or a[1][1]<0

class Ring:
 def __init__(self,v):
  self.v=v;self.mod=cyclo[2*v];self.d=len(self.mod)-1;self.zero=(0,)*self.d;self.one=(1,)+(0,)*(self.d-1)
  self.omega=self.reduce([0,1]);self.powers=[self.one]
  for k in range(1,2*v):self.powers.append(self.mul(self.powers[-1],self.omega))
 def reduce(self,a):
  a=list(a)+[0]*max(0,self.d-len(a))
  for k in range(len(a)-1,self.d-1,-1):
   c=a[k]
   for j in range(self.d+1):a[k-self.d+j]-=c*self.mod[j]
  return tuple(a[:self.d])
 def add(self,a,b):return tuple(x+y for x,y in zip(a,b))
 def neg(self,a):return tuple(-x for x in a)
 def mul(self,a,b):
  out=[0]*(2*self.d-1)
  for i,x in enumerate(a):
   for j,y in enumerate(b):out[i+j]+=x*y
  return self.reduce(out)
 def interval(self,a):
  re=(0,0);im=(0,0)
  for j,x in enumerate(a):
   if x:
    sn,cs=trig_pi(j,self.v)
    re=add(re,scale(cs,x));im=sub(im,scale(sn,x))
  return(re,im)

def canon(s):return min(s[i:]+s[:i] for s in(s,s[::-1]) for i in range(N))
FULL = '--all-words' in sys.argv
words=([format(x,'013b') for x in range(1,2**N-1)] if FULL else
       sorted({canon(format(x,'013b')) for x in range(1,2**N-1)}))
assert len(words)==(8190 if FULL else 378)
allcert=[];start=time.time()
for iw,w in enumerate(words):
 v=w.count('1');ring=Ring(v);B=[0]
 for b in w[:-1]:B.append(B[-1]+int(b))
 exps=[v*k-N*B[k] for k in range(N)];lo=min(exps);hi=max(exps)
 P=[ring.zero]*(hi-lo+1)
 for k,e in enumerate(exps):
  c=ring.powers[B[k]%(2*v)]
  if k%2:c=ring.neg(c)
  P[e-lo]=ring.add(P[e-lo],c)
 r=pow(13,-1,2*v)
 F=[ring.powers[(r*(12-j))%(2*v)] for j in range(13)]
 # Exact monic division by regular-configuration factor.
 rem=P[:];Q=[ring.zero]*(len(P)-12)
 for k in range(len(P)-13,-1,-1):
  c=rem[k+12];Q[k]=c
  for j,f in enumerate(F):rem[k+j]=ring.add(rem[k+j],ring.neg(ring.mul(c,f)))
 assert all(a==ring.zero for a in rem),(w,'regular factor failure')
 # Remove all exact roots z=1 (collapsed configurations).
 endpoint_order=0
 while True:
  val=ring.zero
  for a in Q:val=ring.add(val,a)
  if val!=ring.zero:break
  assert len(Q)>1
  q=[ring.zero]*(len(Q)-1);q[-1]=Q[-1]
  for k in range(len(q)-2,-1,-1):q[k]=ring.add(Q[k+1],q[k+1])
  assert ring.add(Q[0],q[0])==ring.zero
  Q=q;endpoint_order+=1
 coeff=[ring.interval(a) for a in Q]
 stack=[(0,1,0)];accepted=[];maxdepth=0
 while stack:
  left,right,depth=stack.pop();den=2**depth
  # theta in [pi*left/(13*v*den),pi*right/(13*v*den)].
  sl,cl=trig_pi(left,13*v*den);sr,cr=trig_pi(right,13*v*den)
  z=((cr[0],cl[1]),(-sr[1],-sl[0]))
  val=coeff[-1]
  for c in reversed(coeff[:-1]):val=cadd(cmul(val,z),c)
  if zero_excluded(val):
   accepted.append((left,right,depth));maxdepth=max(maxdepth,depth)
  else:
   if depth>=30:raise RuntimeError((w,'inconclusive',left,right,depth,val))
   stack.append((left*2+1,right*2,depth+1));stack.append((left*2,left*2+1,depth+1))
 cert={'word':w,'v':v,'degree_P':len(P)-1,'degree_Q':len(Q)-1,'removed_z1':endpoint_order,'intervals':len(accepted),'max_depth':maxdepth,'partition':accepted}
 allcert.append(cert)
 if iw%(1000 if FULL else 25)==0:print(iw+1,w,'intervals',len(accepted),'depth',maxdepth,'seconds',round(time.time()-start,2),flush=True)
output_name='cycle13_allwords_certificate.json' if FULL else 'cycle13_certificate.json'
with Path(__file__).with_name(output_name).open('w') as f:json.dump({'arithmetic':'integer fixed-point outward intervals','scale':str(S),'words':len(words),'total_intervals':sum(c['intervals'] for c in allcert),'max_depth':max(c['max_depth'] for c in allcert),'certificates':allcert},f,indent=2)
print('PROVED',len(words),'cases;',sum(c['intervals'] for c in allcert),'intervals; max depth',max(c['max_depth'] for c in allcert),'elapsed',time.time()-start,flush=True)

\end{lstlisting}