Written on the Wall II -… to Written on the Wall II -…

TheoremWritten on the Wall II - Conjecture 327#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture327.conjecture327

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/6e85aabe821e6ddf718d050a5bd8f19a48e4f2d9/FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean#L233.

WOWII Conjecture 327

Let G be a simple connected graph. If 3 · γ(G) = γ_i(G), then G is well totally dominated, where γ(G) is the domination number of G and γ_i(G) is the independent domination number of G.

Proof Sketch: The conjecture states that if \(3\gamma(G) = i(G)\) for a connected graph \(G\), then \(G\) is well totally dominated. However, this conjecture is FALSE.

Counterexample: Consider a graph \(G\) with 12 vertices: \(u, v, a_0, a_1, a_2, a_3, a_4, b_0, b_1, b_2, b_3, b_4\). The edges are: - \((u, v)\) - \((u, a_i)\) for all \(i \in \{0, 1, 2, 3, 4\}\) - \((v, b_i)\) for all \(i \in \{0, 1, 2, 3, 4\}\) - \((a_0, b_3), (a_1, b_3), (a_2, b_0), (a_3, b_0), (a_4, b_3), (a_4, b_4)\)

Properties of \(G\): 1. Connected: Yes, path exists between any two vertices through \(u\) and \(v\). 2. Domination Number \(\gamma(G)\): The set \(\{u, v\}\) dominates all vertices. Since there is no universal vertex, \(\gamma(G) = 2\). 3. Independent Domination Number \(i(G)\): The minimum independent dominating set has size 6 (e.g., \(\{u, b_0, b_1, b_2, b_3, b_4\}\)). Thus \(i(G) = 6\). 4. Condition: \(3 \gamma(G) = 3 \times 2 = 6 = i(G)\). The condition holds. 5. Well Totally Dominated: A graph is well totally dominated if all minimal total dominating sets have the same size. - \(\{u, v\}\) is a minimal total dominating set of size 2. - \(\{v, b_0, b_3\}\) is a minimal total dominating set of size 3. Since \(2 \neq 3\), \(G\) is NOT well totally dominated.

The counterexample has been found by Moritz Firsching and Goran Žužić using an experimental pipeline.

theorem conjecture327 :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (_hG : G.Connected)
      (_h : 3 * G.dominationNumber = G.indepDominationNumber),
      IsWellTotallyDominated G

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean, line 70.

Sources
LeanWrittenOnTheWallII.GraphConjecture327.conjecture327

TheoremWritten on the Wall II - Conjecture 430a#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

The conjecture is false for the nonuniform clique blow-up of P₇ with blob orders (1,4,12,19,12,4,1). Its independent domination number is three, its center-neighborhood independence number is two, and its Caro--Wei sum is less than two. The claimed inequality therefore becomes 3 ≤ 2.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture430a.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture430a.conjecture430a

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/c5-k4/blob/85fff48cdd7cc1f743802320fdc94db14d1f841e/lean/GraphConjecture430a.lean#L1-L390.

WOWII Conjecture 430a asked whether every connected graph G of order greater than three satisfies i(G) ≤ α(G[N(C)]) + 2 floor(CW(G)-1). The answer is no, witnessed by a nonuniform P₇ clique blow-up.

theorem conjecture430a :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] [Nonempty V]
      (G : SimpleGraph V) [DecidableRel G.Adj],
      G.Connected → 3 < Fintype.card V →
        (G.indepDominationNumber : ℤ) ≤
          ((G.induce
            (setNeighborhood G (centerFinset G) : Set V)).indepNum : ℤ) +
            2 * ⌊caroWei G - 1⌋

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture430a.lean, line 65.

Sources
LeanWrittenOnTheWallII.GraphConjecture430a.conjecture430a

TheoremWritten on the Wall II - Conjecture 438b#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

WOWII 438b asks whether

alpha₂(G) ≤ alpha(G) + alpha(G[V \ H₂]) + |E(G[H₂])|,

where H₂ is the set of vertices of degree at most two. The conjecture is true. In fact, the same inequality holds with an arbitrary vertex subset in place of H₂.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture438b.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture438b.conjecture438b

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/c5-k4/blob/e62f216625438bc099707e466d2825ab483717a4/lean/GraphConjecture438b.lean.

WOWII 438b states that every connected graph of order greater than three satisfies alpha₂(G) ≤ alpha(G) + alpha(G[V \ H₂]) + |E(G[H₂])|.

theorem conjecture438b :
    ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
      [DecidableRel G.Adj], G.Connected → 3 < Fintype.card V →
      alphaTwo G ≤ G.indepNum +
        indepNumOn G (Finset.univ \ lowDegreeLayer G) +
        (internalEdges G (lowDegreeLayer G)).card

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture438b.lean, line 50.

Sources
LeanWrittenOnTheWallII.GraphConjecture438b.conjecture438b

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.