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

If ϵ is an Erdős–Hajnal constant for H and W is a nonempty vertex set with ∣W∣ϵ>hom⁡(G), then G[W] has an induced copy of H

Statement

Let H be a finite simple graph and let ϵ>0 be an Erdős–Hajnal constant for the hereditary class of H-free graphs. Let G be a finite simple graph and let W⊆V(G) be nonempty with ∣W∣ϵ>hom⁡(G). Then G[W] has an induced copy of H.

Facts & Assumptions

Given: A finite simple graph H, an Erdős–Hajnal constant ϵ>0 for the class of H-free graphs, a finite simple graph G, and a nonempty W⊆V(G) with ∣W∣ϵ>hom⁡(G).

[F1]

A real ϵ>0 is an Erdős–Hajnal constant for a hereditary class C when every nonempty J∈C satisfies hom⁡(J)≥∣V(J)∣ϵ (The Erdős–Hajnal property and an Erdős–Hajnal constant for a hereditary graph class, Real powers for positive bases, with the zero-base positive-exponent convention).

[L1]

For every family F of finite graphs, the class of F-free finite graphs is hereditary (Every class defined by forbidden induced subgraphs is hereditary).

[L2]

hom⁡(G[W])≤hom⁡(G) for every W⊆V(G) (hom⁡(G[W])≤hom⁡(G) for every vertex subset W).

[F4]

Proof

technique · contrapositive
1.1contrapositive-reduce

It suffices to prove the contrapositive: if G[W] has no induced copy of H, then ∣W∣ϵ≤hom⁡(G).

1.2assume-hypF2L1

Assume G[W] has no induced copy of H. Then G[W] is H-free, and the class of H-free graphs is hereditary, so G[W] is a member of the class for which ϵ is an Erdős–Hajnal constant.

2.1step 1.2F1F3F4given

The graph G[W] is nonempty, since W≠∅ and V(G[W])=W, so [F1] applies to it and gives hom⁡(G[W])≥∣W∣ϵ.

3.1step 2.1L2discharge-contrapositive∎

By [L2] we have hom⁡(G)≥hom⁡(G[W]), so hom⁡(G)≥∣W∣ϵ, which is the conclusion of the contrapositive; the Statement follows.

Depends on

Used by

Dependency tree · two levels

17 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