Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-31
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Anticonnected block contraction turns an upside-down comb into a pure blockade

Statement

Let G be a P5-free graph, let k4 be an integer, and let BV(G). Suppose

((ai,Bi):i[k])

is a (k,B/k8)-comb in G with BiB and aiB for every i[k]. Suppose also that there is a vertex

vV(G)(B{a1,,ak})

that is complete to B and anticomplete to {a1,,ak}. Then G[B] contains a pure (k,B/k10)-blockade.

Facts & Assumptions

Given: The graph G, the integer k, the set B, the displayed comb, and the vertex v satisfying the hypotheses above.

[F1]

In the displayed comb, ai is complete to Bi and anticomplete to Bj for ij, while the blocks are pairwise disjoint and satisfy BiB/k8 (Combs in a graph).

[F2]

A set D is an anticonnected component of G[X] precisely when it is the vertex set of a connected component of G[X] (Anticonnected graphs and anticonnected components).

[L1]

Distinct anticonnected components of a graph are complete to one another (Distinct connected components are anticomplete, and distinct anticonnected components are complete).

[F3]

A blockade is pure when every pair of distinct blocks is either complete or anticomplete (Complete, anticomplete, pure, weakly sparse, and x-sparse blockades).

[F5]

Complementation exchanges edges and nonedges (Graph isomorphisms, automorphisms and graph complements).

Proof

technique · contract each comb block to a large anticomponent
1.1

Fix i[k] and put ni:=Bi. Suppose first that every anticonnected component of G[Bi] has size less than ni/k. Partition the anticonnected components into a minimum number of unions S0,,Sr, each of size less than ni/k, and order them by nondecreasing size. Since the parts cover Bi, one has r+1>k. Minimality gives Sj1+Sjni/k for j1, and hence Sjni/(2k)ni/k2 because k4. By [L1], the sets S1,,Sk are pairwise complete. They therefore form a complete, hence pure, (k,ni/k2)-blockade in G[B]. By [F1], ni/k2B/k10, which proves the result in this case.

F1L1F3givenchoosealgebra
2.1

We may consequently assume that, for every i[k], the graph G[Bi] has an anticonnected component Di with DiBi/k. Choose one such Di. Then DiBi/kB/k9B/k10, giving the required width bound for every chosen component.

F1F2step 1.1choosealgebra
3.1

Let ij, and suppose that some uDj is mixed on Di. The sets of neighbours and nonneighbours of u in Di are both nonempty. Since G[Di] is connected, some edge of that complement crosses these two sets. Thus there are w,zDi such that uwE(G), uzE(G), and wzE(G).

F2step 2.1given
4.1

Among the five vertices v,ai,u,z,w, the nonedges are exactly vai,aiu,uz,zw. Indeed, the hypotheses on v determine its four incidences; [F1] determines the incidences from ai to DiBi and to uDjBj; and step 3.1 determines the three remaining incidences. Hence those four nonedges form the path vaiuzw, so these vertices induce P5 by [F4] and [F5], contrary to the hypothesis on G. Therefore no vertex of Dj is mixed on Di.

F1F4F5step 3.1given
5.1

Applying step 4.1 with both orders of i,j shows that no vertex of either set is mixed on the other. If the pair (Di,Dj) had both an edge and a nonedge, then the vertices of Dj would include one complete to Di and one anticomplete to Di; every endpoint in Di of the cross-edge would then be mixed on Dj, a contradiction. Thus (Di,Dj) is pure.

step 4.1cases
6.1

The sets D1,,Dk are pairwise disjoint subsets of B, have size at least B/k10 by step 2.1, and every cross-pair is pure by step 5.1. Hence they form the required pure (k,B/k10)-blockade in G[B].

F1F3step 2.1step 5.1

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources