Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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 can be thinned to equal subblocks with directional sparsity

Statement

Let a≥0, let ϵ∈(0,14], and let

A=(A1,…,Aℓ)

be a blockade in a graph G with ℓ=⌈ϵ−1⌉ and width at least m>0. Assume that every distinct pair (Ai,Aj) is either complete or weakly ϵa-sparse. Then there is a subblockade

D=(D1,…,Dℓ)

such that:

  1. Di⊆Ai and ∣Di∣=⌈ϵ⌈m⌉⌉ for every i∈[ℓ];
  2. if (Ai,Aj) is complete, then (Di,Dj) is complete; and
  3. if (Ai,Aj) is weakly ϵa-sparse, then Di is ϵa−5-sparse to Dj and Dj is ϵa−5-sparse to Di.

Facts & Assumptions

Given: The blockade A=(A1,…,Aℓ) with ℓ=⌈ϵ−1⌉, width at least m, and the complete or weakly ϵa-sparse hypothesis on each distinct pair of blocks.

[L1]

A weakly c-sparse ordered pair (X,Y) satisfies eG(X,Y)≤c∣X∣∣Y∣ by definition (Sparsity of one vertex set to another, and weak sparsity of a pair).

[L2]

A complete pair stays complete after passing to subsets (Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs).

[L3]

Expectation is linear for finite families of random variables, without an independence hypothesis (Expectation is linear for every finite family of random variables, without any independence hypothesis).

[L4]

The probability of a finite union of events is at most the sum of their probabilities (The finite union bound).

Proof

technique · use finite averaging to choose equal ambient blocks with controlled edge counts, then delete vertices that are too heavy against the chosen ambient blocks
1.1givenL1L2L3L4choosealgebra

Put n:=⌈m⌉ and s:=⌈ϵn⌉. Since every ∣Ai∣ is an integer at least m, one has n≤∣Ai∣. Choose independently and uniformly an n-element subset Xi⊆Ai for each i. For a weakly ϵa-sparse pair (Ai,Aj), finite double counting and [L3] give E eG(Xi,Xj)=eG(Ai,Aj)n2∣Ai∣∣Aj∣≤ϵan2. Consequently the probability that eG(Xi,Xj)>ϵa−2n2 is less than ϵ2: on that event the nonnegative edge count already exceeds the threshold, so its expectation is greater than the threshold times the event probability. There are at most (ℓ2) relevant pairs, and (ℓ2)ϵ2<1+ϵ2<1 because ℓ=⌈ϵ−1⌉<ϵ−1+1. By [L4], some simultaneous choice of the Xi therefore satisfies eG(Xi,Xj)≤ϵa−2n2 for every weakly sparse pair. Complete pairs remain complete by [L2]. Fix such a choice.

2.1step 1.1L1choosealgebra

We choose D1,…,Dℓ successively, always requiring Di⊆Xi and ∣Di∣=s. Suppose that D1,…,Di−1 have already been chosen. For each p≠i with (Ap,Ai) weakly ϵa-sparse, let Cp⊆Xi consist of the vertices having more than ϵa−4n neighbours in Dp when p<i, or more than ϵa−4n neighbours in Xp when p>i. In either case step 1.1 gives eG(Xi,Dp)≤eG(Xi,Xp)≤ϵa−2n2, so ∣Cp∣<ϵ2n. Since ℓ−1<ϵ−1, the union of the forbidden sets has fewer than ϵn vertices and therefore at most s−1 vertices. Thus at least n−s+1≥s vertices survive: indeed s≤⌈n/4⌉ and 2⌈n/4⌉≤n+1. Choose Di to be any s survivors.

3.1step 2.1algebra

Let (Ai,Aj) be weakly ϵa-sparse, and assume i<j. When Di was chosen, the index j was still future, so every vertex of Di has at most ϵa−4n neighbours in Xj, hence at most that many in Dj. When Dj was chosen, every vertex of Dj was required to have at most ϵa−4n neighbours in Di. Since s≥ϵn, ϵa−4n≤ϵa−5s. Therefore Di is ϵa−5-sparse to Dj and Dj is ϵa−5-sparse to Di.

4.1

If (Ai,Aj) is complete, then (Di,Dj) is complete by [L2] because Di⊆Ai and Dj⊆Aj. Together with step 3.1, this proves that D=(D1,…,Dℓ) has all the required properties. ∎

Depends on

Used by

Dependency tree · two levels

16 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