Documentation

FormalConjectures.WrittenOnTheWallII.GraphConjecture145

Written on the Wall II - Conjecture 145 #

The WOWII HTML uses $\lambda_{\min}(\overline{G})$ (the bar denotes graph complement). The formal statement below uses the local-independence minimum of $G^c$.

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

Definitions #

The local independence minimum $\mathrm{lMin}(G)$ is: $$\mathrm{lMin}(G) = \min_{v \in V(G)} l(v)$$ where $l(v) = \mathrm{indepNeighborsCard}(G, v)$ is the independence number of the neighbourhood of $v$. This is the minimum over all vertices of the local independence number.

The boundary vertices $B(G)$ of a connected graph are the vertices $v$ such that the eccentricity of $v$ equals the diameter of $G$.

The eccentricity of a set $\mathrm{ecc}(S) = \max_{u \notin S} \min_{w \in S} \mathrm{dist}(u, w)$. In the conjecture below, $\mathrm{ecc}(B)$ is the eccentricity of the boundary set.

Conjecture 145: $\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \lambda_{\min}(\overline{G})$ where $\mathrm{tree}(G)$ is largestInducedTreeSize G, $\mathrm{ecc}(B)$ is the eccentricity of the boundary vertices, and $\lambda_{\min}(\overline{G})$ is the local independence minimum of the complement $\overline{G}$.

source
noncomputable def WrittenOnTheWallII.GraphConjecture145.localIndependenceMin {α : Type u_1} [Fintype α] [Nontrivial α] (G : SimpleGraph α) :
ℕ

localIndependenceMin G is the minimum over all vertices of the local independence number indepNeighborsCard G v. This equals $\mathrm{lMin}$ from DeLaVina's notation.

Equations
Instances For
    source
    theorem WrittenOnTheWallII.GraphConjecture145.conjecture145 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) (hlMin : 0 < localIndependenceMin Gᶜ) :
    2 * G.eccSet G.maxEccentricityVertices ≤ G.largestInducedTreeSize * localIndependenceMin Gᶜ

    WOWII Conjecture 145

    For a simple connected graph $G$, $\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \lambda_{\min}(\overline{G})$ where $\mathrm{tree}(G)$ is the number of vertices in a largest induced subtree, $\mathrm{ecc}(B)$ is the eccentricity of the boundary vertices (eccSet and boundaryVertices), and $\lambda_{\min}(\overline{G})$ is the minimum local independence number of the complement graph.

    We state the inequality in the form $\mathrm{tree}(G) \cdot \mathrm{lMin}(\overline{G}) \ge 2 \cdot \mathrm{ecc}(B)$ to avoid division.