"""Exact checks of supplied external objections, separate from initial prompts.

This verifies finite algebra and elementary integrals, not the full paper or
the proposed replacement thinness and Lyapunov proofs.
"""
from pathlib import Path
from fractions import Fraction
import hashlib, json
import sympy as s

import argparse
parser=argparse.ArgumentParser(description=__doc__)
parser.add_argument('--source',type=Path,required=True,help='The frozen manuscript.tex from the reading packet')
source=parser.parse_args().source
assert source.is_file(), 'Supply the frozen manuscript with --source'
r=s.sqrt(5);phi=(1+r)/2
H=s.Matrix([[2,1],[1,1]])
J=s.Matrix([[2,-1],[-1,1]])
A=H**3;B=J**3
lam=9+4*r;small=9-4*r
u=s.Matrix([phi,1])/s.sqrt(phi**2+1)
v=s.Matrix([phi,-1])/s.sqrt(phi**2+1)
assert A.det()==B.det()==1 and A*B!=B*A
for matrix in (A,B):
    assert {s.simplify(e) for e in matrix.eigenvals()}=={lam,small}
    assert matrix==matrix.T
assert all(s.simplify(x)==0 for x in A*u-lam*u)
assert all(s.simplify(x)==0 for x in B*v-lam*v)
assert s.simplify(u.dot(u))==s.simplify(v.dot(v))==1
cross=s.simplify(u.dot(v));assert s.simplify(cross**2)==s.Rational(1,5)>s.Rational(1,9)
observed=s.simplify((A.inv()*u).dot(A.inv()*u))
assert s.simplify(observed-small**2)==0
assert s.simplify((lam/3)**2-observed)>0

y=s.symbols('y',nonnegative=True)
T=s.symbols('T',positive=True)  # The theorem uses T=2 log(eta)>0; T=0 normalization is checked below.
# 8 exp(-3y) sinh(y) = 4(exp(-2y)-exp(-4y)).
density=4*(s.exp(-2*y)-s.exp(-4*y))
assert s.integrate(density,(y,0,s.oo))==1
tail=s.simplify(s.integrate(density,(y,T,s.oo)))
assert s.simplify(tail-(2*s.exp(-2*T)-s.exp(-4*T)))==0
eta=5
tail5=2*Fraction(1,eta**4)-Fraction(1,eta**8)
bound5=Fraction(1,eta**4)
assert tail5>bound5

result={
 'schema':1,'origin':'coordinator_exact_symbolic_checks_not_model_or_formal_certificate',
 'source_sha256':hashlib.sha256(source.read_bytes()).hexdigest(),
 'sympy_version':s.__version__,
 'lemma_5_2':{'A':A.tolist(),'B':B.tolist(),
   'complete_singular_spectra':['9+4*sqrt(5)','9-4*sqrt(5)'],
   'all_four_forward_inverse_operator_norms':'9+4*sqrt(5)',
   'cross_inner_product_squared':'1/5 > 1/9',
   'self_inner_products':1,'word':'A inverse',
   'observed_action_norm':'9-4*sqrt(5)',
   'claimed_lower_bound':'(9+4*sqrt(5))/3',
   'status':'exact_counterexample_to_native_statement'},
 'theorem_3_4':{'normalized_limiting_gap_density':'8 exp(-3y) sinh(y), y>=0',
   'tail':'2 exp(-2T)-exp(-4T)',
   'eta':eta,'exact_tail_at_2log_eta':str(tail5),'claimed_upper_bound':str(bound5),
   'status':'integral_identity_checked; limiting-measure justification supplied separately'},
 'uniform_free_walk':{'conditional_outward_probability':str(Fraction(3,4)),
   'conditional_inward_probability':str(Fraction(1,4)),
   'conditional_drift_away_from_identity':str(Fraction(3,4)-Fraction(1,4)),
   'qualification':'Finite transition calculation; almost-sure speed requires the separate free-walk argument.'},
 'qualification':'Does not verify angular counting, generic Zariski density, repaired main theorem, or uniform-in-word-length cone proof.'}
print(json.dumps(result,indent=2,default=lambda x:int(x)))