Prove Written on the Wall II Conjecture 316

[DomTheDeveloper]

Proves the genuinely research-open Written on the Wall II Conjecture 316 from Google DeepMind's Formal Conjectures corpus.

Main structural result: under the complement-average-degree hypothesis, a connected graph either is complete, has all vertices pendant, or has a non-pendant core that is a clique of size at most three. The minimal total dominating sets can then be classified explicitly.

Verification:

• exact theorem signature from FormalConjectures.WrittenOnTheWallII.GraphConjecture316;
• Lean 4.27.0 against pinned Formal Conjectures commit b2e608fc52d765510915a244bb69b1a2741acc3c;
• complete lake build passed: 8055 jobs;
• source guard found no sorry, admit, or native_decide;
• #print axioms conjecture316_solved reports only propext, Classical.choice, and Quot.sound;
• final sorryAx rejection guard passed.

This is a machine-verified proof candidate for a statement currently labelled research open. Mathematical novelty and prior-art status still require expert/community review before claiming publication-level resolution.