A Triangle-Free Reduction for the Average Local Independence–leaf Inequality

For a finite simple graph G, let a_G(v) = α(G[N_G(v)]) and let L(G) be the maximum number of degree-one vertices in a spanning tree of G. We prove the following structural reduction: every finite simple graph G has a spanning triangle-free subgraph H with the same connected components as G and e(H) ≥ (1/2) Σv ∈ V(G) a_G(v). The coefficient 1/2 is best possible, already for triangle-free graphs. Equivalently, if τ_△(G) is the minimum number of edges meeting every triangle and τ is the vertex-cover number, then τ_△(G) ≤ (1/2) Σv ∈ V(G) τ(G[N_G(v)]). Combining the reduction with an elementary degree-sum argument for connected triangle-free graphs gives a short alternative proof of the inequality L(G) ≥ 2((1/|V(G)|) Σv ∈ V(G) a_G(v) − 1). This inequality originated as a Graffiti conjecture and was recently proved, with a Lean verification, by Tsoukalas et al. Our contribution is the triangle-free reduction and the resulting proof route. We also state the one-vertex case explicitly, which is excluded by the nontrivial-type assumption in the available Lean formalization.