ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Every hereditary graph class of bounded order has the Erdős–Hajnal property

Example

Let $C$ be a hereditary graph class for which some $N \in N$ satisfies $∣ V (G) ∣ \leq N$ for every $G \in C$ . Then $C$ has the Erdős–Hajnal property.

Facts & Assumptions

Given: A hereditary class $C$ and a natural number $N$ bounding the order of every member.

[L1]

The definition applies to hereditary classes and asks for one $ϵ > 0$ such that every nonempty $G$ satisfies $hom (G) \geq ∣ V (G) ∣^{ϵ}$ (The Erdős–Hajnal property and an Erdős–Hajnal constant for a hereditary graph class).

[L2]

The homogeneous number is the larger of the clique and stable-set numbers (Homogeneous vertex sets and the homogeneous number $hom (G) = \max {ω (G), α (G)}$ ).

[L3]

The logarithm is strictly increasing, satisfies $\log 1 = 0$ , and obeys the quotient law (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L4]

For $a > 0$ and $x \in R$ , $a^{x} : = \exp (x \log a)$ (Real powers for positive bases, with the zero-base positive-exponent convention).

[L5]

$\log : (0, \infty) \to R$ is the inverse function of $\exp$ ; in particular $\exp (\log x) = x$ for $x > 0$ and $\log (\exp y) = y$ for $y \in R$ (The natural logarithm as the inverse of the exponential function).

Verification

technique · cases

1.1

[assume-case small] If $N \leq 1$ , choose $ϵ = 1$ ; every nonempty member has one vertex and homogeneous number $1$ by [L2].

givenL1L2

1.2

[assume-case large] If $N \geq 2$ , choose $ϵ = 1$ when $N = 2$ , and choose $ϵ = \log 2 / \log N$ when $N > 2$ . In the latter case $\log N > \log 2 > \log 1 = 0$ by [L3], so $ϵ > 0$ , and [L4] with [L5] gives $N^{ϵ} = \exp ((\log 2 / \log N) \log N) = \exp (\log 2) = 2$ .

L3L4L5algebrachoose

2.1

Since $\log$ is a strictly increasing bijection onto $R$ with inverse $\exp$ , the function $\exp$ is strictly increasing as well; so for $1 \leq n \leq N$ the inequality $ϵ \log n \leq ϵ \log N$ gives $n^{ϵ} \leq N^{ϵ} = 2$ by [L4].

step 1.2L3L4L5algebra

3.1

In the large case, a graph of order $n \geq 2$ has either an edge, which is a two-vertex clique, or a nonedge, which is a two-vertex stable set; hence $hom (G) \geq 2 \geq n^{ϵ}$ by step 2.1, while for $n = 1$ both sides equal $1$ . The given hereditary hypothesis places $C$ in the domain of [L1].

givenstep 2.1L1L2algebra

4.1

The cases are exhaustive, and in each [L1] supplies the Erdős–Hajnal property.

step 1.1step 3.1L1cases-exhaustive∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 50 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Erdos-Hajnal properties in graphs and hypergraphs, introduction (standard reference, not scraped)