LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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.

A star-expansion of a forest containing a long path contains the corresponding cycle

Statement

Let $r \geq 1$ , and let $F$ be a forest containing an induced path on vertices $b_{1}, \dots, b_{r + 1}$ in this order, and let $F^{⋆}$ be the star-expansion of $F$ . Then $F^{⋆}$ contains an induced cycle on

$r + 4$

vertices.

Facts & Assumptions

Given: An integer $r \geq 1$ , a forest $F$ containing the induced path $b_{1} - b_{2} - \dots - b_{r + 1}$ , and its star-expansion $F^{⋆}$ with root $v$ and teeth $a_{1}, \dots, a_{r + 1}$ matched to those path vertices.

[L1]

In the star-expansion, the only new edges are $v a_{i}$ and $a_{i} b_{i}$ (The star-expansion of a graph).

Proof

technique · direct finite check

1.1

Consider the vertex set ${v, a_{1}, b_{1}, \dots, b_{r + 1}, a_{r + 1}}$ . Along this set the displayed edges $v a_{1}, a_{1} b_{1}, b_{1} b_{2}, \dots, b_{r} b_{r + 1}, b_{r + 1} a_{r + 1}, a_{r + 1} v$ form a cycle of length $r + 4$ .

given

2.1

No other edge joins two vertices of this set. The forest path contributes only the consecutive edges $b_{i} b_{i + 1}$ , since it is induced in $F$ , and [L1] shows that $a_{1}$ and $a_{r + 1}$ meet only their matched path vertices and the root. Hence the chosen vertices induce exactly that cycle.

step 1.1L1

3.1

Therefore $F^{⋆}$ contains an induced cycle on $r + 4$ vertices.

step 2.1∎

Depends on

Used by

A cycle of length at least five and a forest complement have the Erdős-Hajnal property Theorem

Dependency tree · two levels

11 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

Maria Chudnovsky, Alex Scott, Paul Seymour, and Sophie Spirkl, Erdős-Hajnal for graphs with no 5-hole, sentence after Theorem 7.2 (standard reference, not scraped)