"""Finite exact rank/degree checks supporting, not replacing, the proof."""
from pathlib import Path
import hashlib, json
import sympy as z

root=Path(__file__).resolve().parents[1]
rank_checks=[]
for p in range(1,7):
    for q in range(p):
        source=[(i,p-i,j,q-j) for i in range(p+1) for j in range(q+1)]
        target=[(i,p-1-i,j,q+1-j) for i in range(p) for j in range(q+2)]
        indices={a:i for i,a in enumerate(target)}
        matrix=z.zeros(len(target),len(source))
        for col,(a,b,c,d) in enumerate(source):
            if a: matrix[indices[(a-1,b,c+1,d)],col]+=a
            if b: matrix[indices[(a,b-1,c,d+1)],col]+=b
        rank=matrix.rank()
        assert rank==len(source)
        rank_checks.append({'p':p,'q':q,'domain_dimension':len(source),'rank':rank})
U1,U2,Y1,Y2=z.symbols('U1 U2 Y1 Y2')
def D(f):return Y1*z.diff(f,U1)+Y2*z.diff(f,U2)
def E(f):return U1*z.diff(f,Y1)+U2*z.diff(f,Y2)
boundary=U1*Y2-U2*Y1
assert z.expand(D(boundary))==0
commutator_checks=0
for p in range(5):
    for q in range(5):
        for i in range(p+1):
            for j in range(q+1):
                f=U1**i*U2**(p-i)*Y1**j*Y2**(q-j)
                assert z.expand(E(D(f))-D(E(f))-(p-q)*f)==0
                commutator_checks+=1
degree_checks=[]
for a in range(2,21):
    r=a-1;b=a*(a-1);m=b-r
    first=[b-i+1-r for i in range(1,m+1)]
    second=[b-j-((i-1)*r+j) for i in range(1,r+1) for j in range(r)]
    assert min(first)>0 and min(second)>0 and m>=r*(r-1)
    degree_checks.append({'a':a,'endpoint_b':b,'m':m,'first_min_gap':min(first),'second_min_gap':min(second)})
record={'method':'finite exact two-coordinate tests and endpoint ledgers; no general theorem certificate',
        'sympy_version':z.__version__,'source_sha256':hashlib.sha256((root/'sources/native/build/paper.tex').read_bytes()).hexdigest(),
        'rank_checks':rank_checks,'commutator_monomials_checked':commutator_checks,
        'equal_degree_noninjectivity_witness':'U1*Y2-U2*Y1','degree_checks':degree_checks}
(root/'outputs/independent_calculations.json').write_text(json.dumps(record,indent=2)+'\n')
print(json.dumps({'rank_cases':len(rank_checks),'commutator_monomials_checked':commutator_checks,'endpoint_ledgers':len(degree_checks)}))