Disproof of Mukwembi's Theorem 2.1 via Q₃ (3-cube)

[henrykmichalewski]

Summary

• Formal disproof of Theorem 2.1 from Mukwembi, Size, Order, and Connected Domination, Canad. Math. Bull. 57 (2014), 141–144
• The 3-dimensional hypercube Q₃ is a counterexample: n=8, m=12, γ_c=4, bound=11 < 12
• The paper's proof (p. 143) asserts γ_c(G) ≤ γ_c(G − {u,v}) without justification; this is false for Q₃ where γ_c(G') = 2 < 4 = γ_c(Q₃) for every edge
• Corollaries 2.2 and 2.3 remain true (proved independently via GraphConjecture2.lean)

Files

File	Description
Q3Counterexample.lean	Full Lean 4 proof: γ_c(Q₃) = 4, triangle-free, 12 > 11
Q3SafeVerifyTarget.lean	SafeVerify target: Mukwembi's bound with sorry
Q3SafeVerifySubmission.lean	SafeVerify disproof: negation proved without native_decide
SizeOrderConnectedDomination.lean	Lemma 1.2, Eq (1.1), Cor 2.2, Cor 2.3
COUNTEREXAMPLE.md	Detailed writeup with proof gap analysis
COUNTEREXAMPLE.pdf	PDF version
Q3_counterexample.py	Computational verification

SafeVerify disproof verification

Verified using SafeVerify's --disproofs mode (GasStationManager/SafeVerify#16):

• mukwembi_size_bound.disproof proves ∃ G, Connected G ∧ CliqueFree 3 G ∧ ¬(m ≤ bound)
• All 26 declarations replayed, only standard axioms used
• SafeVerify check passed.

Test plan

• Q3Counterexample.lean compiles with lake build (57s, uses native_decide)
• Q3SafeVerifySubmission.lean compiles (no native_decide, uses decide with increased limits)
• SafeVerify --disproofs check passes
• CI build on upstream

🤖 Generated with Claude Code

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[henrykmichalewski]

It is just an edge case that I noticed - the paper may be just fine (my understanding of the concepts may be incorrecT).