"""Exact finite checks for the separately written BK lifting repair.

The all-modulus proof is the determinant argument in reconciliation.md.
Finite checks do not verify spectral counting or the density-one theorem.
Run: python3 check_lifting.py > lifting-results.json
"""
from math import factorial, gcd
from functools import reduce
from itertools import product
import json
import random
import sympy as s


def integral_kernel(a):
    kernel=a.nullspace()
    assert kernel
    w=kernel[0]
    denominator=s.ilcm(*[z.q for z in w])
    w=[int(denominator*z) for z in w]
    common=reduce(gcd,w)
    return [z//abs(common) for z in w]


def main():
    rng=random.Random(220110955)
    cases=[]
    for trial in range(36):
        h=1+trial%6
        u=s.eye(4)
        for i in range(4):
            for j in range(i+1,4):u[i,j]=rng.randint(-2,2)
        inv=u.inv()
        rows=[s.Matrix([[1,0,0,0]]),s.Matrix([[1,1,0,0]]),
              s.Matrix([[1,0,1,0]]),s.Matrix([[1,0,0,1]])]
        rows += [s.Matrix([[1]+[rng.randint(-h,h) for _ in range(3)]]) for _ in range(5)]
        rows=[row*inv for row in rows]
        bound=max(abs(int(z)) for row in rows for z in row)
        q=[2**50,3**36,2**22*5**24][trial%3]
        assert q>120*bound**4
        v=u*s.Matrix([1]+[q*rng.randint(-100,100) for _ in range(3)])
        residue=1
        assert reduce(gcd,[int(z) for z in v])==1
        assert all((int((row*v)[0])-residue)%q==0 for row in rows)
        a=s.Matrix([list(row)+[-1] for row in rows])
        assert a.rank()==4
        star=integral_kernel(a)
        assert any(star[:4]) and a*s.Matrix(star)==s.zeros(len(rows),1)
        g=reduce(gcd,star[:4]);assert star[4]%g==0
        primitive=[z//abs(g) for z in star]
        assert reduce(gcd,primitive[:4])==1 and a*s.Matrix(primitive)==s.zeros(len(rows),1)
        cases.append({'case':trial,'modulus':q,'row_height':bound,'determinant_bound':120*bound**4,
                      'rank':4,'primitive_lift':primitive})
    # Zero rows and an empty S impose no constraint on the nonzero vector.
    for a in [s.zeros(0,5),s.Matrix([[0,0,0,0,-1]])]:
        w=integral_kernel(a);assert any(w[:4]) and a*s.Matrix(w)==s.zeros(a.rows,1)
    # Full rank: a primitive modular solution can exist when q is small.
    a=s.Matrix([[1,0,0,0,-1],[-1,0,0,0,-1],
                [0,1,0,0,-1],[0,0,1,0,-1],[0,0,0,1,-1]])
    w=s.ones(5,1);assert all(z%2==0 for z in a*w)
    det=int(a.det());assert abs(det)==2 and not a.nullspace()
    adj=a.adjugate();assert adj*a==det*s.eye(5)
    # Modular primitivity is essential: a vector divisible by q can always
    # solve the homogeneous congruence of a full-rank matrix.
    q=2**50;w=s.Matrix([q,0,0,0,0]);assert all(z%q==0 for z in a*w)
    assert reduce(gcd,[int(z) for z in w[:4]]+[q])==q
    # Test the finite-field degree-three root bound and bounded-shear choice.
    prime_checks=0
    for prime in [5,7]:
        for v in product(range(prime),repeat=4):
            if not any(v):continue
            bad=[t for t in range(prime) if sum(v[j]*t**j for j in range(4))%prime==0]
            assert len(bad)<=3
            assert any(sum(v[j]*t**j for j in range(4))%prime for t in range(4))
            prime_checks+=1
    composite_checks=[]
    for primes,exponents in [([7],[3]),([7,11],[2,1]),([11,13,17],[1,2,1])]:
        q=1
        for prime,e in zip(primes,exponents):q*=prime**e
        length=len(primes);assert min(primes)>3*length
        for trial in range(50):
            while True:
                v=[rng.randrange(q) for _ in range(4)]
                if reduce(gcd,v+[q])==1:break
            possible=[t for t in range(3*length+1) if gcd(sum(v[j]*t**j for j in range(4)),q)==1]
            assert possible
            t=possible[0];u=s.eye(4);u[0,:]=s.Matrix([[1,t,t*t,t*t*t]])
            assert u.det()==1 and all(z.q==1 for z in u.inv())
        composite_checks.append({'modulus':q,'distinct_prime_divisors':primes,'cases':50})
    print(json.dumps({'arithmetic':'exact integers and rational matrices; SymPy '+s.__version__,
                      'scope':'Finite checks and negative controls; all-modulus proof supplied separately. No spectral or headline-theorem certificate.',
                      'lifting_cases':cases,'edge_cases':['empty S','all row vectors zero'],
                      'negative_controls':{'small_modulus_full_rank_determinant':det,'nonprimitive_modular_vector':'full rank remains possible'},
                      'prime_polynomial_checks':prime_checks,'composite_shear_checks':composite_checks,
                      'all_assertions_passed':True},indent=2))


if __name__=='__main__':main()