"""Exhaustive SL_2(F_p) checks for two BGS local-density counterexamples.

Standard library; exact integer arithmetic throughout. This checks finite cases;
the proof for every odd prime is in comparison-and-repair.md.
"""
from fractions import Fraction
from math import prod
import json
import platform


def main():
    rows = []
    for p in (3, 5, 7, 11, 13, 17, 19, 23, 29, 31):
        group = count_sum = count_plus_one = 0
        for a in range(p):
            for b in range(p):
                completions = sum((a*d-b*c) % p == 1
                                  for c in range(p) for d in range(p))
                group += completions
                if (a*a+b*b) % p == 0:
                    count_sum += completions
                if (a*a+1) % p == 0:
                    count_plus_one += completions
        assert group == p*(p*p-1)
        expected_sum = 0 if p % 4 == 3 else 2*p*(p-1)
        expected_plus_one = 0 if p % 4 == 3 else 2*p*p
        assert count_sum == expected_sum
        assert count_plus_one == expected_plus_one
        rows.append({'prime':p, 'group_order':group,
                     'zeros_a2_plus_b2':count_sum,
                     'beta_a2_plus_b2':str(Fraction(count_sum,group)),
                     'zeros_a2_plus_1':count_plus_one,
                     'beta_a2_plus_1':str(Fraction(count_plus_one,group))})
    # Exact CRT ratio |Lambda_m^f|/m^2, for square-free products of split primes.
    composite = []
    primes = (5,13,17,29,37,41,53)
    for k in range(1,len(primes)+1):
        m = prod(primes[:k])
        ratio = prod(Fraction(2*(p-1),p) for p in primes[:k])
        composite.append({'number_of_prime_factors':k,'modulus':m,
                          'ratio_to_m2':str(ratio)})
    print(json.dumps({'arithmetic':'exact integers and fractions',
                      'python':platform.python_version(),
                      'method':'enumerate every first row and all second rows; test determinant one',
                      'all_assertions_passed':True,
                      'prime_cases':rows,'crt_ratios':composite},indent=2))


if __name__ == '__main__':
    main()