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 E theorem reaches an induced P5 witness

Example

The five-vertex path P5 is E-free but is not P5-free. More generally every P5-free graph is E-free, because the vertices p1,…,p5 of E induce P5. Thus the E-free theorem applies to a strictly larger forbidden-pattern class than the earlier P5-free theorem.

Facts & Assumptions

Given: The E-graph on {p1,…,p5,q}, the path P5 on {0,1,2,3,4}, and an arbitrary finite graph G.

[L1]

The E-graph has vertex set {p1,p2,p3,p4,p5,q} and edge set {p1p2,p2p3,p3p4,p4p5,p3q} (The E-graph and co-E).

[L2]

The path P5 has vertex set {0,1,2,3,4} and edges {i,i+1} for 0≤i<4, and no others (Empty and complete graphs, complete bipartite graphs, and the convention that Pn and Cn have n vertices).

[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 ϵE>0 such that every nonempty E-free graph has a clique or stable set of size at least ∣V(G)∣ϵE (The E-graph has the Erdős-Hajnal property).

[L5]

The graph P5 has the Erdős-Hajnal property, and an Erdős-Hajnal constant for the P5-free class is a positive exponent bounding the homogeneous number of every nonempty member from below by ∣V(G)∣ to that exponent (The five-vertex path and its complement have 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-$P_5$ restriction
1.1

The identity map on {0,1,2,3,4} preserves adjacency and nonadjacency, so it is an induced embedding of P5 in itself by [L3]; hence P5 is not P5-free.

L2L3
1.2

The six-element set {p1,…,p5,q} has no injection into the five-element set {0,1,2,3,4}; hence no induced embedding of E in P5 exists, and P5 is E-free.

L1L2L3
1.3

Suppose the finite graph G is not E-free. By [L3] there is an induced embedding φ of E in G. Its restriction φ′ to {p1,…,p5} is again an injection preserving adjacency and nonadjacency, and by [L1] the induced subgraph of E on those five vertices has exactly the edges p1p2,p2p3,p3p4,p4p5, which is a P5 under [L2]. So φ′ is an induced embedding of P5 in G, and G is not P5-free. Contrapositively, every P5-free graph is E-free.

L1L2L3
2.1

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

step 1.1step 1.2step 1.3
3.1

The E theorem [L4] bounds every nonempty graph in the larger E-free class, hence in particular every nonempty graph in the P5-free class, whereas the earlier P5 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 P5, 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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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