from fractions import Fraction
from itertools import product
import json, random
import sympy as sp

u,y=sp.symbols('u y')
def mons(U,Y): return [(i,j) for i in range(U+1) for j in range(Y+1)]
def dict_poly(expr): return sp.Poly(sp.expand(expr),u,y).as_dict()
def exact_system(m,g,U,Y):
    cols=[]; rows=set()
    for i,j in mons(U,Y):
        h=u**i*y**j; z=dict_poly(m*u*sp.diff(h,u)*sp.diff(g,y)-sp.diff(h,y)*(g+m*u*sp.diff(g,u)))
        cols.append(z); rows.update(z)
    rows=sorted(rows|{(0,0)})
    A=sp.polys.matrices.DomainMatrix.from_list_sympy(len(rows),len(cols),[[col.get(r,0) for col in cols] for r in rows])
    Ab=sp.polys.matrices.DomainMatrix.from_list_sympy(len(rows),len(cols)+1,[[col.get(r,0) for col in cols]+[1 if r==(0,0) else 0] for r in rows])
    return A.rank(),Ab.rank(),len(cols),len(rows)

# New exhaustive exact low-bidegree attack: all 80 nonconstant g=1+a*u+b*y+c*u*y, coefficients {-1,0,1}.
solvable=[]; tested=0; basis=[u,y,u*y]
for m in (1,2,3,4,5):
  for cs in product((-1,0,1),repeat=3):
    if not any(cs):continue
    g=1+sum(c*z for c,z in zip(cs,basis)); tested+=1
    rank,aug,ncols,nrows=exact_system(m,g,4,5)
    if rank==aug:solvable.append({'m':m,'g':str(g),'rank':rank,'unknowns':ncols,'equations':nrows})
assert not solvable,solvable[:3]

# New exact rational substitutions against weighted-edge identity.
rng=random.Random(22072026); edge_checks=0; attempts=0
while edge_checks<500 and attempts<5000:
    attempts+=1;m=rng.randint(1,8);q=rng.randint(1,6);p=rng.randint(0,6)
    if sp.gcd(p,q)!=1:continue
    r=rng.randrange(q);s=rng.randint(1,6);sigma=sp.Rational(q*s-p*r,q)
    if sigma<=0:continue
    N=rng.randint(0,5);D=rng.randint(1,5);T=sp.Symbol('T');t=u**q*y**p
    phi=[sp.Rational(rng.randint(-5,5),rng.randint(1,5)) for _ in range(N+1)];A=[sp.Rational(rng.randint(-5,5),rng.randint(1,5)) for _ in range(D+1)]
    phi[-1]=sp.Rational(rng.randint(1,5),rng.randint(1,5));A[-1]=sp.Rational(rng.randint(1,5),rng.randint(1,5))
    Phi=sum(phi[i]*T**i for i in range(N+1));At=sum(A[i]*T**i for i in range(D+1));H=u**r*y**s*Phi.subs(T,t);g=At.subs(T,t)
    got=sp.expand(m*u*sp.diff(H,u)*sp.diff(g,y)-sp.diff(H,y)*(g+m*u*sp.diff(g,u)))
    B=-p*T*At*sp.diff(Phi,T)-s*At*Phi-m*q*sigma*T*sp.diff(At,T)*Phi
    assert sp.expand(got-u**r*y**(s-1)*B.subs(T,t))==0;edge_checks+=1
out={'status':'PASS','method':'new exhaustive exact rational rank systems plus exact rational edge substitutions','coefficient_systems_tested':tested,'g_family':'1+a*u+b*y+c*u*y','g_coefficient_domain':[-1,0,1],'H_bidegree_caps':[4,5],'m_values':[1,2,3,4,5],'solvable_nonconstant_cases':len(solvable),'weighted_edge_exact_rational_checks':edge_checks,'seed':22072026}
with open(r'C:\Users\Studio\AppData\Roaming\AGNT\projects\proofkit-report-iv-independent-search-results.json','w',encoding='utf-8') as f:json.dump(out,f,indent=2)
print(json.dumps(out,indent=2))
