Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-04
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.

A complete-or-weakly-sparse blockade yields a complete subblockade or an anticonnected thinning

Statement

Let ϵ∈(0,14], let ℓ=⌈ϵ−1⌉, and let

D=(D1,…,Dℓ)

be a blockade in a graph G such that all blocks have the same size q>1 and every distinct pair (Di,Dj) is either complete or mutually η-sparse. Then one of the following holds:

  1. G contains a complete (ℓ,q/ℓ2)-blockade; or
  2. there exist anticonnected subsets Bi⊆Di with ∣Bi∣=⌈q/ℓ⌉ for all i∈[ℓ] such that every distinct pair (Bi,Bj) is either complete or mutually (ηℓ)-sparse.

Facts & Assumptions

Given: The blockade D=(D1,…,Dℓ) of common block size q>1 and the complete or mutually η-sparse hypothesis on each distinct pair.

[L1]
[L2]

An anticonnected component is, by definition, an inclusion-maximal anticonnected induced subgraph (Anticonnected graphs and anticonnected components).

Proof

technique · inspect each block's anticonnected components
1.1givenchooseL1algebra

Suppose some block Di has no anticonnected component of size at least q/ℓ. Partition the anticonnected components of G[Di] into a minimum number of nonempty unions S0,…,Sr, each of size less than q/ℓ, ordered so that ∣S0∣≤⋯≤∣Sr∣. Since the unions cover Di and each has size less than q/ℓ, one has r+1>ℓ. Minimality implies ∣St−1∣+∣St∣≥q/ℓ for every t≥1, for otherwise those two unions could be merged. Hence ∣St∣≥q/(2ℓ)≥q/ℓ2 for every t≥1, because ℓ≥2. Distinct anticonnected components are complete to one another by [L1], so distinct unions of them are also complete to one another. Therefore S1,…,Sℓ form a complete (ℓ,q/ℓ2)-blockade, proving outcome 1.

2.1step 1.1chooseL2

We may therefore assume that every Di has an anticonnected component Ci of size at least q/ℓ. By [L2], the complement G[Ci]‾ is connected. Choose a spanning tree of G[Ci]‾, and repeatedly delete leaves until exactly ⌈q/ℓ⌉ vertices remain. The remaining tree is connected, so the induced subgraph of G[Ci]‾ on those vertices is connected as well. Calling that vertex set Bi, we have Bi⊆Ci, ∣Bi∣=⌈q/ℓ⌉, and G[Bi] anticonnected.

3.1step 2.1algebra

If (Di,Dj) is complete, then (Bi,Bj) is complete because Bi⊆Di and Bj⊆Dj. If (Di,Dj) is mutually η-sparse, every vertex of Bi has at most η∣Dj∣=ηq neighbours in Dj, hence at most ηq≤ηℓ∣Bj∣ neighbours in Bj because ∣Bj∣≥q/ℓ; the same argument with i and j exchanged gives the reverse direction. Thus every noncomplete pair is mutually (ηℓ)-sparse.

4.1step 1.1step 2.1step 3.1∎

Step 1.1 yields outcome 1, while steps 2.1 and 3.1 yield outcome 2. Therefore one of the two stated outcomes holds.

Depends on

Used by

Dependency tree · two levels

18 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