∑ Math Proof PlaygroundWOWII › 322

WOWII Graph Conjecture 322

A short structural proof: the local-independence hypothesis forces the graph to be complete, and every minimal total dominating set then has size two.

complete human proofLean CI pendingexact Formal Conjectures statement

Theorem

If G is connected, |V(G)| ≥ 5, and α(G[N(v)]) ≤ 1 for every vertex v, then G is well totally dominated.

The proof is stronger than the catalogued statement: the lower bound |V(G)| ≥ 5 is not used.

The structural collapse

  1. If two distinct vertices u,w are both neighbors of v, then they must be adjacent. Otherwise {u,w} is an independent two-set inside G[N(v)], contradicting α(G[N(v)]) ≤ 1.
  2. Thus every open neighborhood is a clique.
  3. Along any connected walk, two consecutive edges can be shortcut. Induction collapses a walk between distinct endpoints to a single edge.
  4. Therefore every two distinct vertices are adjacent: G is complete.

Total domination in a complete graph

A total dominating set cannot have one vertex because vertices have no loops. Every pair of distinct vertices is total dominating. Hence any total dominating set with more than two vertices contains a smaller total dominating pair and is not minimal. All minimal total dominating sets therefore have cardinality exactly two.

Verification status

LayerStatus
Human proofComplete
Exact Lean theoremFull proof written and independently audited
Upstream submissionFormal Conjectures PR is under review

Artifacts

Submission artifacts

Verification & provenance

CRL proof archive. Status is updated only when the cited verification evidence changes.