LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Relative to a complete nonedge pair in a co- $E$ -free graph, a one-sided vertex mixed on an induced path avoids two consecutive nonneighbours and three consecutive neighbours

Statement

Let $G$ be co- $E$ -free, let $P$ be an induced path, and let distinct vertices $x, y \notin V (P)$ be nonadjacent and complete to $P$ . If $u \in N (x) ∖ N (y)$ is mixed on $P$ , then $u$ has neither two consecutive nonneighbours nor three consecutive neighbours on $P$ .

Facts & Assumptions

Given: $G, P, x, y, u$ as in the Statement.

[F1]

In co- $E$ , adjacency is the complement of the five-path-with-middle-leaf edge set defining $E$ (The $E$ -graph and co- $E$ ).

[F2]

A path has distinct vertices and its listed consecutive edges, while an induced copy preserves both adjacency and nonadjacency. Hence an induced path has precisely its consecutive path edges among its own vertices (Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges, Induced embeddings and induced copies of a graph).

Proof

technique · contradiction

1.1

Suppose two consecutive vertices of $P$ are nonneighbours of $u$ . Travelling from a neighbour of $u$ on $P$ to the first such consecutive pair and taking the first change gives an induced subpath $a - b - c$ with $u a$ an edge and $u b, u c$ nonedges.

givenF2assume-contra

1.2

If instead $u$ has three consecutive neighbours, reverse $P$ if needed and take the last such run before an adjacency change. There is an induced subpath $a - b - c - d$ with $u a, u b, u c$ edges and $u d$ a nonedge.

givenF2construct

2.1

On ${x, y, u, a, b, c}$ the nonedges are exactly the $E$ -edges under $(p_{1}, p_{2}, p_{3}, p_{4}, p_{5}, q) = (x, y, u, c, a, b)$ : they are $x y, y u, u c, c a, u b$ . Thus this induced subgraph is co- $E$ , contrary to [F1].

step 1.1F1F2contradiction

2.2

On ${y, u, a, b, c, d}$ the nonedges are exactly the $E$ -edges under $(p_{1}, p_{2}, p_{3}, p_{4}, p_{5}, q) = (c, a, d, u, y, b)$ : they are $c a, a d, d u, u y, d b$ . This is an induced co- $E$ , again a contradiction.

step 1.2F1F2contradiction

3.1

Both assumed runs are impossible, proving the two assertions.

step 2.1step 2.2discharge-contradiction∎

Depends on

Used by

Dependency tree · two levels

10 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

Huang, Ju, and Zhou, Erdős-Hajnal beyond the five-vertex path, Claim 6.4.1 (standard reference, not scraped)

Relative to a complete nonedge pair in a co-EE-free graph, a one-sided vertex mixed on an induced path avoids two consecutive nonneighbours and three consecutive neighbours