"""Exact checks for source-adjudicated Yang findings; not a formal proof certificate. The all-parameter arguments and norm qualifications are in additional-checks.md. No manuscript code is executed. No provider API is called. """ from pathlib import Path import argparse import hashlib import json import sympy as s parser = argparse.ArgumentParser() parser.add_argument('--source', type=Path, required=True) parser.add_argument('--output', type=Path, required=True) args = parser.parse_args() source = args.source.read_bytes() assert hashlib.sha256(source).hexdigest() == 'e6f3ee5af078764b1750ea6a8cdbc8c1d9577ef6d14d0bc638830f385d839db8' def E(i,j): m=s.zeros(3);m[i-1,j-1]=1;return m u, us = E(2,3), E(3,2) a = s.diag(0,s.Rational(1,2),-s.Rational(1,2)) a0 = s.diag(s.Rational(1,3),-s.Rational(1,6),-s.Rational(1,6)) v1,v2,w1,w2 = E(2,1),E(3,1),E(1,3),E(1,2) comm=lambda x,y:x*y-y*x def contains(m,basis): coords=s.Matrix.hstack(*(v.reshape(9,1) for v in basis)) return coords.row_join(m.reshape(9,1)).rank()==coords.rank() plus=[v1,w1];minus=[v2,w2];bracket_checks=0 for x in plus: for y in minus: assert contains(comm(x,y),[a,a0]);bracket_checks+=1 for h in [a,a0]: assert contains(comm(x,h),plus);bracket_checks+=1 assert contains(comm(x,us),minus) and comm(x,u)==s.zeros(3);bracket_checks+=2 for x in minus: for h in [a,a0]: assert contains(comm(x,h),minus);bracket_checks+=1 assert contains(comm(x,u),plus) and comm(x,us)==s.zeros(3);bracket_checks+=2 for x in plus: for y in plus: assert contains(comm(x,y),[u]);bracket_checks+=1 for x in minus: for y in minus: assert contains(comm(x,y),[us]);bracket_checks+=1 for h in [a,u,us]: assert comm(a0,h)==s.zeros(3);bracket_checks+=1 assert comm(a,u)==u and comm(a,us)==-us and comm(u,us)==2*a;bracket_checks+=3 # D fixes the H-volume vector but lies outside A0 H (negative first coordinate). D=s.diag(-1,-1,1) images=[D*h*D.inv() for h in [a,u,us]] assert images==[a,-u,-us] assert s.diag(1,-1,-1).det()==1 and D[0,0]<0 # An integral matrix with nontrivial commuting unipotent part need not be unipotent. gs=s.diag(1,-1,-1);gu=s.eye(3)-u;gamma=gs*gu assert gamma==s.Matrix([[1,0,0],[0,-1,1],[0,0,-1]]) assert gamma.det()==1 and gs*gu==gu*gs and gu!=s.eye(3) assert (gu-s.eye(3))**2==s.zeros(3) assert gamma.trace()==-1 and gamma**2==s.eye(3)-2*u # Exact Ad weights: z=exp(ell/6). The printed positive conjugation is reversed. z=s.symbols('z',positive=True) A=s.diag(z**2,1/z,1/z) for v in [v1,v2]:assert A*v*A.inv()==z**-3*v for w in [w1,w2]:assert A*w*A.inv()==z**3*w assert z**-6*z**-3==z**-9 and z**-6*z**3==z**-3 # Literal scalar inference and conditional probability inequality. assert s.Rational(1,2)**30 < s.Rational(1,2)**22 mass=s.Rational(1,4);subset=s.Rational(1,8) assert subset/mass==s.Rational(1,2)>subset # Hyperbola comparison. Exact identity, then rational bounds valid for all # beta<=1/10, q>=10, q^2>=2/beta^2. y ranges in [-3 beta/(5q),3 beta/(5q)]. beta,q,y=s.symbols('beta q y',positive=True) w=beta*q/2;wp=w+1/(beta*q) f=-y/(1+w*y);fp=-y/(1+wp*y) assert s.simplify(f-fp+(wp-w)*y**2/((1+w*y)*(1+wp*y)))==0 assert s.Rational(3,10)*s.Rational(1,10)**2+s.Rational(3,5)/10**2 < s.Rational(1,2) assert s.Rational(36,25)*s.Rational(1,10)<1 assert s.simplify(4*(wp-w)*(3*beta/(5*q))**2)==36*beta/(25*q**3) assert s.simplify((wp-w)/(1/q))==1/beta numeric_beta=s.Rational(1,100);numeric_q=s.Integer(10000) assert numeric_q**2>=2/numeric_beta**2 # Compatibility of sufficient hyperbola parameter inequalities with paper scales. # theta in (0,1e-10), N1=1e31/theta, epsilon^3=exp(-3e36/theta). # exp(x)>x gives b b_upper.subs(theta,s.Rational(1,10)**10) # Exact boundary separation example: ell=1, r1=beta/4, v=e beta u/4. # e<3 follows from its factorial series, so ||v||<3 beta/40, # delta_h is h-close to delta_0 on Lip<=1 tests, but any exact convex # representation delta_h=(1-eps)delta_0+eps nu requires eps=1. assert (1-s.Rational(1,10))>0 result={ 'origin':'coordinator_exact_symbolic_and_rational_checks_not_formal_verification', 'source_sha256':hashlib.sha256(source).hexdigest(), 'checker_sha256':hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), 'sympy_version':s.__version__, 'lemma_2_1_bracket_checks':bracket_checks, 'stabilizer_counterexample':{'matrix':D.tolist(),'action_on_H_basis':[1,-1,-1],'exterior_cube_multiplier':1,'excluded_from_A0H':'first entry -1; A0H first entry is positive'}, 'unipotent_assertion_counterexample':{'matrix':gamma.tolist(),'semisimple_part':gs.tolist(),'unipotent_part':gu.tolist(),'trace':-1,'square':(gamma**2).tolist()}, 'positive_conjugation_weights':{'r1':'exp(-ell/2)','r2':'exp(ell/2)','thin_r1_after_positive_conjugation':'beta exp(-3ell/2)','r2_after_positive_conjugation':'beta exp(ell/2)','negative_conjugation_balances':'beta exp(-ell/2) in both'}, 'hyperbola_family':{'w':'beta q/2','w_prime':'beta q/2+1/(beta q)','k':1,'k_prime':1,'ell':0,'A':1,'q':'exp(s_prime)','sufficient_conditions':['0=10','q^2>=2/beta^2','q^(-10 C1 epsilon1)<=beta/2'],'graph_distance_upper_bound':'(36/25) beta q^-3 < q^-3','parameter_gap_over_claimed_bound':'beta^-1','source_scales_compatible':True}, 'separation_example':{'ell':1,'beta':'16^-4','x':'Gamma','r1':'beta/4','r2':0,'r3':0,'v':'e beta u/4','norm_qualification':'coordinate/Frobenius; e<3 gives ||v||=1 lemma; does not refute a corrected large-ell application'}, 'conditioning_example':{'mass_P':'1/4','mass_A':'1/8','conditional_mass':'1/2','scope':'counterexample to the claimed inference from conditioning alone, not to the dynamical lemma'}, 'limitations':['All-integer and analytic arguments are in accompanying notes.','No repaired main theorem is proved.','Finite exact algebra is not a formal proof certificate.'] } args.output.write_text(json.dumps(result,indent=2,default=str)+'\n') print(json.dumps({'status':'passed','bracket_checks':bracket_checks,'output':str(args.output)}))