Patrick and I have a long list of -properties and -bounds to code. Independence Number Theory be viewed as whatever properties and invariants we’ve already coded. So we can generate graphs which are “difficult” with respect to the coded theory. In our current minimal configuration, a 5-cycle with a chord popped out as difficult. This graph has a vertex v such that the graph induced on N[v] is complete. It can be argued that such a vertex is in some maximum independent set. This graph can be reduced. So the graph tells us what -property to code next.
Addendum: this process has continued. With the limited theory coded so far, a graph that was “almost KE” popped out, so that property was added, then a graph that was claw-free, so that property was added. Then the following graph popped out:
Notice that if you remove edge 6-0 you get a KE graph. We call the property where removal of some edge yields a KE graph, “almost-edge-KE”. It can be argued that the independence number of an almost-edge-KE graph G can be efficiently computed. Either G has a non-empty KE part, or every non-empty independent set has more neighbors, and . It can then be argued that, if n is odd, so n=2k+1, then , and if n is even, so n=2k, then