Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27
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.

The Bird theorem reaches an induced bull witness

Example

The five-vertex bull is Bird-free but is not bull-free. Every bull-free graph is Bird-free, since deleting Bird's added leaf w leaves an induced bull. Hence the Bird-free theorem covers a strictly larger forbidden-pattern class than the earlier bull-free theorem.

Facts & Assumptions

Given: The Bird graph on {x1,x2,x3,y,z,w}, the bull on {x1,x2,x3,y,z}, and an arbitrary finite graph G.

[L1]

The Bird graph has vertex set {x1,x2,x3,y,z,w} and edge set {x1x2,x2x3,x1x3,x1y,x2z,yw}, so the vertices {x1,x2,x3,y,z} span the bull and w is an added leaf (The Bird graph and co-Bird).

[L2]

The bull has vertex set {x1,x2,x3,y,z} and edge set {x1x2,x2x3,x1x3,x1y,x2z} (The bull graph).

[L3]

An induced embedding of H in G is an injection V(H)→V(G) preserving adjacency and nonadjacency on distinct pairs; G is H-free when no such embedding exists (Induced embeddings and induced copies of a graph, H-free and F-free graphs under the induced-subgraph convention).

[L4]

There is ϵB>0 such that every nonempty Bird-free graph has a clique or stable set of size at least ∣V(G)∣ϵB (The Bird graph has the Erdős-Hajnal property).

[L5]

The bull has the Erdős-Hajnal property, and an Erdős-Hajnal constant for the bull-free class is a positive exponent bounding the homogeneous number of every nonempty member from below by ∣V(G)∣ to that exponent (The bull graph has the Erdős-Hajnal property, The Erdős–Hajnal property and an Erdős–Hajnal constant for a hereditary graph class, Homogeneous vertex sets and the homogeneous number hom⁡(G)=max⁡{ω(G),α(G)}).

Verification

technique · direct finite checks of the two witnesses and the induced-bull restriction
1.1

The identity map on {x1,x2,x3,y,z} preserves adjacency and nonadjacency, so it is an induced embedding of the bull in itself by [L3]; hence the bull is not bull-free.

L2L3
1.2

The six-element set {x1,x2,x3,y,z,w} has no injection into the five-element set {x1,x2,x3,y,z}; hence no induced embedding of Bird in the bull exists, and the bull is Bird-free.

L1L2L3
1.3

Suppose the finite graph G is not Bird-free. By [L3] there is an induced embedding ψ of Bird in G. Its restriction ψ′ to {x1,x2,x3,y,z} is again an injection preserving adjacency and nonadjacency, and by [L1] and [L2] the induced subgraph of Bird on those five vertices is exactly the bull, with the same edge set x1x2,x2x3,x1x3,x1y,x2z. So ψ′ is an induced embedding of the bull in G, and G is not bull-free. Contrapositively, every bull-free graph is Bird-free.

L1L2L3
2.1

By step 1.3 the class of bull-free graphs is contained in the class of Bird-free graphs, and the containment is strict because the bull itself is Bird-free by step 1.2 yet is not bull-free by step 1.1.

step 1.1step 1.2step 1.3
3.1

The Bird theorem [L4] bounds every nonempty graph in the larger Bird-free class, hence in particular every nonempty graph in the bull-free class, whereas the earlier bull theorem [L5] concerns only that smaller class. Since both theorems merely assert the existence of positive exponents, step 2.1 is a strict inclusion of hypothesis classes and implies no comparison between the two exponents.

step 2.1L4L5
4.1

The witness bull, the general inclusion of step 1.3 and the strictness of step 2.1 verify all assertions of the example.

step 2.1step 3.1∎

Remarks

  • This example is a leaf: it is homed on the companion examples page and no later item cites it. It is the Bird analogue of the P5 containment example on the same page.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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