We present a compact systems case study in AI-assisted theorem search centered on five closely related graph families: ladders, prisms, Mobius ladders, forward-diagonal ladders, and forward-diagonal prisms. For each family, the workflow follows the same bounded structure: exact small-n census, conjecture compression, one proof route, canonical proof-note hardening, and hostile validation. The resulting cluster yields exact formulas for the maximum size of a balanced independent set under a fixed parity-class partition, together with explicit lower-bound constructions and signed-word proofs. The central technical organ is a reduction from a fibre-word encoding to a signed parity-class word. In that representation, balancedness becomes a zero-sum constraint, interior occupied adjacencies impose a family law, and the extremal bound follows from either zero-forcing or block-packing. What transfers across the five families is therefore not a complete proof template, but a stable representation plus a disciplined way to isolate the family-specific obstruction. This paper does not claim that all five formulas are mathematically novel. A dedicated novelty audit found mixed status: the ladder, prism, and Mobius-ladder theorems carry meaningful folklore or hidden-prior-art risk, while the diagonal pair appears more promising but is not yet fully literature-cleared. In this paper, hostile validation pressure-tests explicit proof notes and exact-census receipts; it does not replace the proofs. The primary contribution is therefore systems-level rather than pure-combinatorial: a validated five-theorem cluster that demonstrates adjacent transfer, proof hardening, and honest novelty boundaries in a controlled mathematical setting.
Brian Philippe M. Saturnino (Sun,) studied this question.