∑ Math Proof Playground › WOWII › 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
- If two distinct vertices
u,ware both neighbors ofv, then they must be adjacent. Otherwise{u,w}is an independent two-set insideG[N(v)], contradictingα(G[N(v)]) ≤ 1. - Thus every open neighborhood is a clique.
- Along any connected walk, two consecutive edges can be shortcut. Induction collapses a walk between distinct endpoints to a single edge.
- Therefore every two distinct vertices are adjacent:
Gis 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
| Layer | Status |
|---|---|
| Human proof | Complete |
| Exact Lean theorem | Full proof written and independently audited |
| Upstream submission | Formal Conjectures PR is under review |
Artifacts
Submission artifacts
- SUBMIT_NOW.md
- 322.lean — archived submission file
- 322.lean — archived upstream-open snapshot
- ISSUE.md · PR.md
Verification & provenance
CRL proof archive. Status is updated only when the cited verification evidence changes.