"""Small exact checks written from the frozen source, not from panel verdicts."""
from fractions import Fraction
from itertools import combinations, product
from math import comb
import json
from pathlib import Path
import sympy as s

C=s.Matrix([[1+s.I,1-s.I],[1-s.I,1+s.I]])/2
H=s.Matrix([[1,1],[1,-1]])
K=H*s.diag(2,1)*H*s.diag(-3,1)*H
assert s.simplify(C*C)==s.Matrix([[0,1],[1,0]])
assert K==s.Matrix([[-8,-10],[0,-6]])
t=s.symbols('t',nonzero=True)
D=s.diag(4*t/5,1)
assert s.simplify(D*s.diag(-s.Rational(1,8),-s.Rational(1,6))*K*D.inv())==s.Matrix([[1,t],[0,1]])
# Newton factorization at small primitive roots, exactly in Q[z]/Phi_r.
zeta=s.symbols('zeta')
for r in range(2,9):
    phi=s.cyclotomic_poly(r,zeta)
    reduce=lambda p:s.rem(p,phi,zeta)
    inv=lambda p:s.invert(p,phi,zeta)
    entries=[[reduce(zeta**(i*j)) for j in range(r)] for i in range(r)]
    newton=[[reduce(s.prod(zeta**i-zeta**j for j in range(k))) if i>=k else 0 for k in range(r)] for i in range(r)]
    for i,j in product(range(r),repeat=2):
        value=sum(reduce(newton[i][k]*inv(newton[k][k])*newton[j][k]) for k in range(r))
        assert reduce(value-entries[i][j])==0
# The scalar incidence identity is independent of the enormous chosen h.
triples=list(combinations(range(7),3))
RG=s.Matrix([[s.Rational(len(set(a)&set(b))-1,2) for b in triples] for a in triples])
JV=s.Matrix([[(1 if a==b else 0)-RG[i,j] for j,b in enumerate(triples)] for i,a in enumerate(triples)])
assert RG+JV==s.eye(len(triples))
assert all(JV[i,j]==0 for i,a in enumerate(triples) for j,b in enumerate(triples) if len(set(a)&set(b)) in (1,3))
# A small arbitrary-content replay checks cancellation without assuming clean storage.
U=s.Matrix([[1,0,0],[2,1,0],[3,4,1]])
T=s.Matrix([[1,2],[3,4],[5,6]])
F=s.Matrix([[1,0,2],[0,3,0]])
direct=s.Matrix([[1,0],[0,2]])
x=s.Matrix(s.symbols('x0:2'));z=s.Matrix(s.symbols('z0:3'))
assert s.expand(F*(U*z+T*x)+direct*x-F*U*z)==(F*T+direct)*x
# Exact CRT/chirp/sector enumeration is a finite identity check, not an asymptotic test.
L=15
assert all((j*k-10*(j%3)*(k%3)-6*(j%5)*(k%5))%L==0 for j in range(L) for k in range(L))
assert all(k*k+j*j-(k-j)**2==2*k*j for j in range(12) for k in range(12))
# Explicit blocks: [2,0],[1] and [1,0],[2],[3].
blocks=[[[2,0],[1]],[[1,0],[2],[3]]]
packed=[]
for chosen in product(*blocks):
    for digits in product(*chosen):packed.append(digits[0]*4+digits[1])
addresses={value:index for index,value in enumerate(packed)}
for b0,b1 in product(range(2),range(3)):
    q0=len(blocks[0][b0]);q1=len(blocks[1][b1])
    p0=sum(map(len,blocks[0][:b0]));p1=sum(map(len,blocks[1][:b1]))
    start=p0*4+q0*p1
    for t0,t1 in product(range(q0),range(q1)):
        value=blocks[0][b0][t0]*4+blocks[1][b1][t1]
        assert addresses[value]==start+t0*q1+t1
h=100;v=comb(h,3);N=v**3;I0=3*v*v;m=h**3
d=comb(h-3,3)+3*(h-3)
W=2*N+I0*(v*d+h+1);Wstar=2**71
delta=2*v*v*(v-3*h*(h+1))
assert W<Wstar and Wstar//2<W
eps=Fraction(delta,m*Wstar)
assert eps==Fraction(1717850673,590295810358705651712)
assert eps>Fraction(28,10**13)
result={'checks':['C squared is swap','three-kernel shear factorization','Newton factorization in cyclotomic fields at widths 2 through 8','incidence cancellation for all triples at h=7','arbitrary-content replay cancellation','coprime Fourier exponents at length 15','chirp exponents','nonconsecutive sector packing','exact network constants and exponent inequality'],
        'h':h,'v':v,'N0':N,'I0':I0,'neighbor_count':d,'W':W,'Wstar':Wstar,'m':m,'delta':delta,'epsilon':str(eps),
        'scope':'Finite exact identities and integer arithmetic only. No complete network, full algorithm, external theorem, Lean build, or asymptotic complexity certified.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps(result,indent=2))