Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

In a regular pair, fewer than ϵ∣X∣ vertices have too small a degree into a large subset, and fewer than ϵ∣X∣ have too large a degree

Statement

Suppose (X,Y) is an ϵ-regular pair of density d, and Y′⊆Y satisfies ∣Y′∣≥ϵ∣Y∣. Then fewer than ϵ∣X∣ vertices x∈X have ∣N(x)∩Y′∣<(d−ϵ)∣Y′∣, and fewer than ϵ∣X∣ vertices have ∣N(x)∩Y′∣>(d+ϵ)∣Y′∣.

Facts & Assumptions

Given: An ϵ-regular pair (X,Y) of density d and a set Y′⊆Y with ∣Y′∣≥ϵ∣Y∣.

[L1]

Every A⊆X, B⊆Y with ∣A∣≥ϵ∣X∣ and ∣B∣≥ϵ∣Y∣ satisfies ∣d(A,B)−d(X,Y)∣≤ϵ (ϵ-regular pairs and self-regular vertex sets).

Proof

technique · contradiction
1.1assume-contragivenchoose

Let A be the set of all x∈X with ∣N(x)∩Y′∣<(d−ϵ)∣Y′∣ and let B be the set of all x∈X with ∣N(x)∩Y′∣>(d+ϵ)∣Y′∣. Suppose, for contradiction, that ∣A∣≥ϵ∣X∣.

2.1step 1.1L1algebra

Summing degrees over A gives e(A,Y′)<(d−ϵ)∣A∣∣Y′∣, hence d(A,Y′)<d−ϵ. Since ∣A∣≥ϵ∣X∣ and ∣Y′∣≥ϵ∣Y∣, this contradicts [L1]. Therefore ∣A∣<ϵ∣X∣.

3.1step 2.1L1algebra

Assume likewise that ∣B∣≥ϵ∣X∣. Summing degrees over B gives d(B,Y′)>d+ϵ, and the same two size conditions again contradict [L1]. Therefore ∣B∣<ϵ∣X∣.

4.1step 2.1step 3.1discharge-contradiction∎

Both exceptional sets therefore have size strictly below ϵ∣X∣, which is the Statement.

Depends on

Used by

Dependency tree · two levels

2 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