"""Constant audit and examples for the bounded-defect parameter theorem.

The infinite assertion is proved by inequalities in the companion note, not
by the finite sequence samples below. No website or database writes.
"""
from fractions import Fraction as F
from pathlib import Path
import importlib.util
import json

ROOT = Path(__file__).resolve().parents[1]
spec = importlib.util.spec_from_file_location('criterion', ROOT/'tools/research-p56-row-criterion-2026-09-08.py')
criterion = importlib.util.module_from_spec(spec)
spec.loader.exec_module(criterion)


def run():
    criterion.certify_pi()
    # Consequences of K>=100 and K>=10D^2: a=1/K<=.01,
    # b=D/K<=1/30, c=D^2/K<=.1. Each check is a uniform endpoint bound.
    a, b = F(1,100), F(1,30)
    checks = {}
    def positive(name, margin):
        assert margin > 0, (name,margin)
        checks[name] = str(margin)

    positive('D_over_K_below_one_thirtieth', F(1,900)-F(1,1000))
    positive('local_epsilon_cap', F(5481,10**6)-a*b/6)
    positive('U_squared_below_seven_sixths_squared', F(49,36)-(F(4,3)+a*b/3))
    positive('U_below_uniform_local_cap', F(1160182,10**6)**2-(F(4,3)+a*b/3))
    positive('L_over_K_below_three_fifths', F(9,25)-(1+a*b)/3)
    positive('n_below_K_squared_over_three', F(1,3)-(F(3,10)+F(4,5)*a+a*a))
    positive('packing_sqrt_coefficient', F(6,7)-F(81,100))
    positive('UD_below_three_over_K', 3*(F(9,20)-a)-F(7,6))
    positive('covering_delta_above_eight_over_five_K', F(1512,539)-F(64,25))
    positive('full_K_step_angle_below_point_one', F(1,10)-b*(F(3,2)+F(13,4)*a))
    positive('projection_barrier', F(8,5)*(1-F(1,200))-1)
    positive('two_ended_angle_coefficient', F(4,5)-(F(3,4)+F(13,4)*a))
    positive('zigzag_error_coefficient', F(5,3)-(F(19,12)+F(33,64)*a*b))
    positive('endpoint_height_coefficient', 4-(F(1,3)+F(13,4)))
    positive('universal_competitor_exclusion', F(1,4)-F(4,125)-F(1,8)-F(1,250))
    assert F(checks['universal_competitor_exclusion']) == F(89,1000)
    # The refined corner choice requires pi/6>14 beta.
    positive('refined_corner_direction', criterion.PL/6-14*a*b/4)

    sequences = []
    for defect, seed in [(2,(19,11)), (3,(12,7)), (11,(17,10)), (12,(24,14))]:
        K,L = seed
        terms = []
        for _ in range(6):
            assert 3*L*L-K*K == defect
            product = (K+1)*(L+1)
            terms.append(dict(K=K,L=L,ns=sorted({product//2,(product+1)//2}),
                M2=str(1+F(L*L,K*K)), theoremApplies=K>=max(100,10*defect*defect)))
            K,L = 2*K+3*L,K+2*L
        sequences.append(dict(defect=defect,terms=terms,asymptotic_n_times_gap=str(F(defect,24))))

    finite = [criterion.inspect(n) for n in [621,1512]]
    assert all(r['status'].startswith('criterion passes') for r in finite)

    # A rigorous counterexample to indefinite constant-ratio scaling (12t,7t).
    t=545
    K,L=12*t,7*t
    K2,L2=6571,3797
    assert (K+1)*(L+1)==(K2+1)*(L2+1)
    assert K2*K2<3*L2*L2 and K2>=L2
    original=1+F(L*L,K*K)
    improved=1+F(L2*L2,K2*K2)
    assert improved < original
    counterexample=dict(t=t,n=(K+1)*(L+1)//2,originalWindow=[K,L],
        improvedWindow=[K2,L2], originalM2=str(original),improvedM2=str(improved),
        exactSquaredImprovement=str(original-improved),
        scope='Analytic construction certificate; no millions-of-points array generated.')

    out=dict(status='Self-reviewed parameter proof, pending later independent review',
        theorem='For integers D=3L^2-K^2>0 and K>=max(100,10D^2), both checkerboard phases are globally optimal at their cardinalities.',
        uniformConstantMargins=checks,sequences=sequences,finitePrefixChecks=finite,
        constantRatioCounterexample=counterexample)
    (ROOT/'docs/p56-defect-families-audit-2026-09-08.json').write_text(json.dumps(out,indent=2)+'\n',encoding='utf-8',newline='\n')
    print(json.dumps(dict(uniformChecks=len(checks),minimumCompetitorMargin='89/1000',
        families=[dict(D=s['defect'],firstNs=[r['ns'] for r in s['terms']],
            firstTheoremWindow=next([r['K'],r['L']] for r in s['terms'] if r['theoremApplies'])) for s in sequences],
        finitePrefixes=[dict(n=r['n'],status=r['status']) for r in finite],
        constantRatioCounterexample=counterexample),indent=2))


if __name__=='__main__':
    run()