"""Exact elementary checks for the corrected definite-form class bound.

For f=A x^2+2Bxy+C y^2 with AC-B^2=a^2, a primitive
representation of z1 puts it in a class with A=z1, so B^2=-a^2 mod z1.
The script tests local root bounds; it does not enumerate all form classes.
"""
from math import gcd
import json
checks=0;worst={}
for p in (2,3,5,7,11):
    Cp=4 if p==2 else 2
    for e in range(1,5):
        m=p**e
        for a in (1,2,3,p,p*p):
            count=sum((b*b+a*a)%m==0 for b in range(m))
            g=gcd(m,a*a)
            assert count*count<=Cp*Cp*g,(p,e,a,count,g)
            checks+=1
    worst[str(p)]={'local_constant_bound':Cp}
# An actual primitive form and primitive represented vector fix the convention.
A,B,C,a,z1=5,2,1,1,5
assert A*C-B*B==a*a
assert (B*B+a*a)%z1==0 and (B*B+4*a*a)%z1!=0
print(json.dumps({'arithmetic':'exact integers','local_cases_checked':checks,'bounds':worst,
    'normalization_witness':{'A':A,'B':B,'C':C,'a':a,'z1':z1,'AC_minus_B_squared':A*C-B*B,
        'ordinary_discriminant':4*(B*B-A*C),'source_negative_four_equals_determinant':False},
    'scope':'Supports the elementary root bound with corrected determinant/discriminant convention; does not certify other imported estimates.'},indent=2))