"""Exact rational witness to the displayed pointwise smoothing assertion.

This checks the written cancellation step only; it is not a counterexample to
uniform coset counting, which could have a different smoothing proof.
"""
import json
from sympy import Matrix,eye,Rational
I=eye(4);Q=2*I-Matrix.ones(4)
S=[]
for i in range(4):
    s=eye(4)
    for j in range(4):s[i,j]=-1 if i==j else 2
    assert s.T*Q*s==Q and s.det()==-1
    S.append(s)
U=S[0]*S[1];V=S[1]*S[2];A=U-I
assert A**3==Matrix.zeros(4)
t=Rational(1,100000)
g=I+t*A+t*(t-1)*A**2/2
assert g.T*Q*g==Q and g.det()==1
eta=Rational(1,100);Y=100
norm2=lambda m:sum(x*x for x in m)
assert norm2(g-I)<eta**2
rows=[]
for k in [10,100,1000]:
    gamma1=V**(7*k);gamma=gamma1.inv()
    assert all(x.q==1 for x in gamma1) and all(x.q==1 for x in gamma)
    assert all(int(x)%7==int(y)%7 for x,y in zip(gamma1,I))
    unperturbed=gamma1*gamma
    perturbed=gamma1*g.inv()*gamma
    assert unperturbed==I and perturbed.T*Q*perturbed==Q
    assert norm2(unperturbed)<(Y*(1-10*eta))**2
    rows.append({'k':k,'gamma1_word':'(S2*S3)^(7*k)','gamma1_congruent_identity_mod_7':True,
        'unperturbed_frobenius_norm_squared':str(norm2(unperturbed)),
        'perturbed_frobenius_norm_squared':str(norm2(perturbed)),
        'perturbed_outside_Y_ball':bool(norm2(perturbed)>Y**2)})
assert any(r['perturbed_outside_Y_ball'] for r in rows)
print(json.dumps({'arithmetic':'exact SymPy rationals','eta':str(eta),'Y':Y,'t':str(t),
    'small_g_distance_squared_from_identity':str(norm2(g-I)),
    'h':'identity','gamma':'gamma1 inverse','cases':rows,
    'interpretation':'Written inner-range cancellation is false for this small g: gamma1*g^-1*gamma is not controlled by gamma1*gamma. Does not refute the counting-lemma conclusion.'},indent=2))