LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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 tournament vertex having an in-neighbour and an out-neighbour on a directed cycle can be inserted into that cycle

Statement

Let $C$ be a directed cycle in a tournament, and let $x$ be a vertex outside $C$ . If some vertex of $C$ sends an arc to $x$ and $x$ sends an arc to some vertex of $C$ , then the tournament has a directed cycle whose vertex set is $V(C)\cup\{x\}$ .

Facts & Assumptions

Given: A directed cycle $C=(c_1,c_2,\ldots,c_k,c_1)$ and an outside vertex $x$ satisfying the two incidence hypotheses.

[F1]

Between $x$ and each $c_i$ , exactly one arc direction occurs (A tournament is an orientation of a complete finite graph).

[F2]

A directed cycle follows its cyclic sequence of arcs and has distinct vertices before returning to its start (Directed walks, trails, paths and cycles, and strong connectivity).

Proof

technique · constructive

1.1

Mark a cycle vertex $c_i$ with $I$ when $c_i x$ is an arc and with $O$ when $xc_i$ is an arc. Both marks occur by hypothesis, and [F1] gives exactly one mark at each cycle vertex. Therefore somewhere around the cyclic order an $I$ -marked vertex $c_i$ is followed by an $O$ -marked vertex $c_{i+1}$ .

givenF1F2

2.1

Replace the cycle arc $c_ic_{i+1}$ by the two arcs $c_ix$ and $xc_{i+1}$ . All other cycle arcs remain unchanged, and $x$ is new, so the resulting closed directed walk is a directed cycle on $V(C)\cup\{x\}$ .

step 1.1F2construct

3.1

This explicitly constructs the required enlarged directed cycle.

step 2.1discharge-construct∎

Depends on

Used by

Camion's theorem: every strongly connected tournament on at least three vertices has a directed Hamilton cycle Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 12 results over 8 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

Encyclopedia of Mathematics, Tournament (standard reference, not scraped)
Robin Wilson, Introduction to Graph Theory (standard reference, not scraped)