Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Induced counting lemma: regular edge and nonedge pairs force many induced copies

Statement

Let H be a graph on labelled vertices [h] and let 0<η<1/2. There are γ=γ(H,η)>0, c=c(H,η)>0, and N=N(H,η) such that the following holds. Let W1,…,Wh be vertex sets of size at least N, with repetitions allowed. Assume every (Wi,Wj), including those with Wi=Wj, is γ-regular. If d(Wi,Wj)≥ηfor ij∈E(H),d(Wi,Wj)≤1−ηfor ij∉E(H), then there are at least c∏i∣Wi∣ injective maps ϕ with ϕ(i)∈Wi that induce H.

Facts & Assumptions

Given: H,η and regular host sets as in the Statement.

[L1]

Regular dense pairs support a greedy count of many part-respecting injective edge-preserving maps of any fixed graph (Counting lemma: regular dense pairs contain many part-respecting copies of every fixed graph).

[L2]

For disjoint sets, complementation preserves the regularity parameter and replaces density d by 1−d (Complementation sends a disjoint ϵ-regular pair of density d to one of density 1−d).

[L3]

An induced embedding is injective and preserves both adjacency and nonadjacency; its labelled count is ind⁡H(G) (Induced embeddings and induced copies of a graph, The induced-embedding count ind⁡H(G)).

Proof

technique · direct
1.1givenL3

Colour each unordered pair ij of pattern vertices by whether it is an edge or a nonedge of H. On an edge pair retain adjacency in the host; on a nonedge pair regard nonadjacency as the required relation.

2.1step 1.1L2algebra

If Wi and Wj are disjoint, [L2] turns the latter relation into a γ-regular pair of complementary density at least η. If the host sets coincide or overlap, the same conclusion for candidate degrees follows directly from the defining regularity inequalities: replace each density d(A,B) by the proportion of distinct ordered pairs in A×B that are nonedges. For candidate sets A⊆Wi and B⊆Wj the coinciding pairs number ∣A∩B∣, so this replacement changes the proportion by at most ∣A∩B∣/(∣A∣∣B∣)≤1/max⁡(∣A∣,∣B∣) — a bound in the current candidate sizes, not in min⁡i∣Wi∣, since candidate sets shrink as the greedy argument proceeds.

3.1step 2.1L1choose

Choose γ small enough for the greedy argument underlying [L1] with density threshold η/2 and all (h2) coloured constraints, and let ρ=ρ(H,η)>0 be the fraction of its host set that every candidate set provably retains throughout that argument, so that every candidate set met in step 2.1 has size at least ρN. Choose N large enough that 1/(ρN)<η/4; then the diagonal error of step 2.1 stays below η/4 at every stage.

4.1step 3.1L1induction

Run that greedy proof with the required relation for each pair. At each stage the typical-degree exclusions occupy only a controlled fraction of the current candidate set, so at least c0∏i∣Wi∣ relation-preserving maps remain for a constant c0=c0(H,η)>0.

5.1step 4.1algebrachoose

At most (h2)N−1∏i∣Wi∣ of these maps have a collision. Enlarge N so this is below c0∏i∣Wi∣/2 and put c=c0/2.

6.1step 1.1step 5.1L3∎

Every surviving map is injective and realizes adjacency exactly on the edges of H, so it is an induced embedding by [L3]. This proves the claimed bound.

Depends on

Used by

Dependency tree · two levels

14 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