"""Exact coordinator checks of the supplied Astra counterexample.

Branch arguments in counterexample.md cover every integer vector for every
L>=10. Finite box checks below are sanity checks, not exhaustive SVP proofs.
No floating-point arithmetic or provider inference is used.
"""
from pathlib import Path
from itertools import combinations,product
from fractions import Fraction
import hashlib,json
import sympy as s
import argparse
parser=argparse.ArgumentParser()
parser.add_argument('--source',type=Path,required=True)
args=parser.parse_args()
source=args.source
g=s.Matrix([[2,s.Rational(2,3),0],[0,1,0],[0,0,s.Rational(1,2)]])
dual=s.Matrix([[s.Rational(1,2),0,0],[-s.Rational(1,3),1,0],[0,0,2]])
assert g.det()==1 and g.inv().T==dual
pairs=list(combinations(range(3),2))
wedge=s.Matrix([[g.extract(i,j).det() for j in pairs] for i in pairs])
hodge=s.Matrix([[0,0,1],[0,-1,0],[1,0,0]])
assert hodge*wedge==dual*hodge
z=s.symbols('z',positive=True);r=s.symbols('r',real=True)
a=s.diag(1,z,1/z);u=s.eye(3);u[1,2]=r
e1=s.Matrix([1,0,0]);assert a*e1==u*e1==e1
big_u=s.eye(3);big_u[1,2]=r*z**2
assert a*u*a.inv()==big_u
q=s.symbols('q',positive=True);a0=s.diag(q**2,1/q,1/q)
assert a0*u==u*a0 and a0*a==a*a0
# q=exp(L/6). For L>=10, exp(5/3)>1+5/3+(5/3)^2/2>4.
assert 1+s.Rational(5,3)+s.Rational(5,3)**2/2>4
# Polynomial inequalities controlling all coordinate branches increase for q>=4.
for value in [Fraction(2*4**3,9),Fraction(4**3,4),Fraction(4**3,2),Fraction(4,3)]:assert value>1
# Enumerate complete integer boxes for rational q as an independent finite check.
box=[s.Matrix(v) for v in product(range(-6,7),repeat=3) if any(v)]
finite=[]
for t in (s.Rational(4),s.Rational(8)):
 d=s.diag(t**2,1/t,1/t)
 matrices=[d*g,d.inv()*dual,d.inv()*g,d*dual]
 expected=[1/(2*t),3/(2*t**2),2/t**2,1/t]
 for matrix,target in zip(matrices,expected):
  euclidean=min((matrix*v).dot(matrix*v) for v in box)
  sup=min(max(abs(x) for x in matrix*v) for v in box)
  assert euclidean==target**2 and sup==target
 finite.append({'q':str(t),'exact_minima_euclidean_and_sup':[str(x) for x in expected]})
# The general family also has arbitrary margins at the critical exponent.
c=s.symbols('c',positive=True);Q=s.symbols('Q',integer=True,positive=True)
fam=s.Matrix([[c,c/Q,0],[0,1,0],[0,0,1/c]])
assert fam.det()==1
assert fam.inv().T==s.Matrix([[1/c,0,0],[-1/Q,1,0],[0,0,c]])
# Conservative exact epsilon bound suffices for the retained-set failure.
delta=Fraction(1,100000);eps_upper=Fraction(1,1000)
gap=2*delta/3-eps_upper**3/4;assert gap>0
# The endpoints are in the theorem window, but need a stronger threshold.
assert Fraction(99,100)<1-delta<1+delta<Fraction(101,100)
# Curve: h=exp(-t/2)/2 -> exp(t) h^2=1/4, exact symbolic identity.
w=s.symbols('w',positive=True);assert s.simplify(w**2*(1/(2*w))**2)==s.Rational(1,4)
result={'origin':'coordinator_exact_symbolic_checks_of_user_supplied_Astra_claim_not_independent_model_or_formal_certificate',
 'source_sha256':hashlib.sha256(source.read_bytes()).hexdigest(),
 'checker_sha256':hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),'sympy_version':s.__version__,
 'matrix':[[str(x) for x in row] for row in g.tolist()],
 'dual_matrix':[[str(x) for x in row] for row in dual.tolist()],
 'determinant':'1','hodge_exterior_square_identity_verified':True,'fixed_vector':'2 e1',
 'all_integer_vector_argument':'See counterexample.md; q=exp(L/6)>=4 for L>=10. Coordinate/disibility cases cover every nonzero vector.',
 'minima_for_L_ge_10':{'positive_standard':'(1/2) exp(-L/6)','positive_dual':'(3/2) exp(-L/3)','negative_standard':'2 exp(-L/3)','negative_dual':'exp(-L/6)'},
 'finite_box_sanity_checks':{'coordinate_range':[-6,6],'nonzero_vectors_per_box':len(box),'checks':finite},
 'thickness_margin_multiple':'at least 3/2 for both signs',
 'retained_set_failure':{'delta1':str(delta),'epsilon_upper_bound':str(eps_upper),'positive_exponent_gap_lower_bound':str(gap),'conclusion':'Every point is removed for all sufficiently large t; F is empty.'},
 'general_family':'Critical coefficients c and Q/c; can exceed every fixed normalization constant.',
 'curve_rescaled_quadratic_remainder':'1/4',
 'limitations':['Exact script uses v6; publication separately compares official journal passages.', 'Branch proofs and fixed-vector measure obstruction are supplied in the accompanying note.', 'No amended theorem or curve corollary is certified by this script.']}
print(json.dumps(result,indent=2))