I'd be interested in whether your data has any cases refuting my conjecture that, when the bound isn't tight, s is still >= m/3
No.
I've implemented a piece of Python that computes your bound (that is, computes *my* statement of it, without attempting to simplify based on this followup) and compared it with all the data I have so far (which is everything up to n=10, and some but not all for n=11).
The complete list of cases I know of in which your bound is not tight (assuming I haven't made any errors in my implementation) is: s(6,7), s(7,8), s(9,10), s(3,11), s(4,11), s(5,11), s(7,11). And in all those cases, we do still have s ≥ m/3. |