"""CC0. Finite trace recovery, exact PG cup checks, and reproducible SVG.
The tests use the existing actual PG1–PG14 index-ten balanced-word model.
They do not construct a new counterexample or supply the general proof.
"""
from fractions import Fraction as F
from pathlib import Path
from itertools import product
from math import isqrt
from html import escape
import json
# Exact Q(sqrt(2)): (a,b) means a+b sqrt(2).
ZERO=(F(0),F(0));ONE=(F(1),F(0))
def qa(x,y):return (x[0]+y[0],x[1]+y[1])
def qm(x,y):return (x[0]*y[0]+2*x[1]*y[1],x[0]*y[1]+x[1]*y[0])
def qs(c,x):return (c*x[0],c*x[1])
def root(x):
for s in [1,2]:
v=x/s;a,b=isqrt(v.numerator),isqrt(v.denominator)
if a*a==v.numerator and b*b==v.denominator:return (F(a,b),F(0)) if s==1 else (F(0),F(a,b))
raise AssertionError(x)
odd=(F(1,4),F(1,2),F(1,4));even=(F(2,5),F(1,5),F(2,5));d=10
weight=lambda j:odd if j%2 else even
def word_weight(w,start=1):
a=F(1)
for j,i in enumerate(w,start):a*=weight(j)[i]
return a
def cup_word(r,i):
if not r:return F(1),[i]
scalar=F(d**(2**(r-1)));out=[]
for k in [2*i,2*i-1,2*i+1,2*i]:
a,b=cup_word(r-1,k);scalar*=a;out+=b
return scalar,out
def apply_cup(v,j):
out={};wts=weight(j)
for w,c in v.items():
old=w[j-1]
if old!=w[j]:continue
for a in range(3):
z=w[:j-1]+(a,a)+w[j+1:];term=qm(c,root(wts[a]*wts[old]));out[z]=qa(out.get(z,ZERO),term)
return {w:c for w,c in out.items() if c!=ZERO}
def apply_block(r,w):
scalar,ops=cup_word(r,1);v={w:ONE}
for j in reversed(ops):v=apply_cup(v,j)
return {w:qs(scalar,c) for w,c in v.items() if c!=ZERO}
def expected_column(k,w):
first=w[:k]
if w[k:]!=first[::-1]:return {}
a=word_weight(first)
return {v+v[::-1]:root(word_weight(v)*a) for v in product(range(3),repeat=k)}
identity=(0,1,2)
def pmul(a,b):return tuple(a[b[i]] for i in range(3))
def charge(w):
p=identity;n=0
for j,i in enumerate(w,1):
if i==1:p=pmul(p,(1,0,2));n+=-1 if j%2 else 1
elif i==2:p=pmul(p,(0,2,1))
return p,n
reports=[]
for r in [0,1,2]:
k=2**r;words=list(product(range(3),repeat=k))
inputs=list(product(range(3),repeat=2*k)) if k<=2 else [w+w[::-1] for w in words]
if k==4:
inputs+=list(w for w in product(range(3),repeat=8) if w[4:]!=w[:4][::-1])[:32]
for w in inputs:assert apply_block(r,w)==expected_column(k,w),(k,w)
assert sum(word_weight(w) for w in words)==1
recovered={w:word_weight(w[::-1],k+1) for w in words}
assert sum(recovered.values())==1
assert all(word_weight(w)*recovered[w]==F(1,d**k) for w in words)
units=0
for a in words:
for b in words:
if charge(a)==charge(b):
# For E_ab, the equation between first and reversed second half is
# exactly equality of these rank-one coefficients on every input.
assert word_weight(a)==word_weight(b)
for c in words[:9]:assert root(word_weight(a)*word_weight(c))==root(word_weight(b)*word_weight(c))
units+=1
reports.append(dict(K=k,original_cup_word_length=len(cup_word(r,1)[1]),original_cup_word_scalar=str(cup_word(r,1)[0]),cup_columns_checked=len(inputs),all_cup_columns_checked=(k<=2),balanced_matrix_units_checked=units,physical_cup_trace=str(F(1,d**k)),recovered_trace_normalization='1'))
assert reports[0]['original_cup_word_scalar']=='1' and reports[1]['original_cup_word_scalar']=='10' and reports[2]['original_cup_word_scalar']=='1000000'
assert sum(odd)==sum(even)==1
assert all(a*b==F(1,10) for a,b in zip(odd,even))
out=[]
def put(s):out.append(s)
def rect(x,y,w,h,fill,stroke='#9aafbd',r=12):put(f'')
def text(x,y,s,size=22,bold=False,anchor='start',fill='#142c42'):put(f'{escape(s)}')
def arrow(x1,y1,x2,y2):put(f'')
put('')
rootdir=Path(__file__).resolve().parent
(rootdir/'standard-model-trace-recovery.svg').write_text('\n'.join(out)+'\n',encoding='utf-8')
if rootdir.name!='figures':
(rootdir/'figure-mathematical-check.json').write_text(json.dumps(dict(actual_model='Existing PG1–PG14; no new model construction',original_first_B_trace=[str(x) for x in odd],recovered_first_trace=[str(x) for x in even],tests=reports,cofinality_is_proved_not_inferred_from_finite_samples=True),indent=2)+'\n',encoding='utf-8')
print(json.dumps(dict(tested_K=[x['K'] for x in reports],cup_columns_checked=sum(x['cup_columns_checked'] for x in reports),balanced_matrix_units_checked=sum(x['balanced_matrix_units_checked'] for x in reports),svg='standard-model-trace-recovery.svg')))