TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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 graph is Hamiltonian if and only if its Bondy-Chvatal closure is Hamiltonian

Statement

A finite simple graph $G$ is Hamiltonian if and only if its Bondy-Chvatal closure $cl (G)$ is Hamiltonian.

Facts & Assumptions

Given: A finite simple graph $G$ .

[L1]

Adding an eligible nonedge preserves Hamiltonicity in both directions (If nonadjacent $u, v$ in an $n$ -vertex graph satisfy $\deg (u) + \deg (v) \geq n$ , then adding $u v$ preserves Hamiltonicity in both directions).

[F1]

The closure is obtained by a finite sequence of eligible edge additions (The Bondy-Chvatal closure of a finite simple graph).

[L2]

The terminal closure is independent of the chosen eligible-addition order (The Bondy-Chvatal closure is independent of the order of eligible edge additions).

[F2]

Hamiltonian means possessing a Hamilton cycle (Hamilton paths, Hamilton cycles, Hamiltonian graphs and Hamilton-connected graphs).

Proof

technique · direct

1.1

Along any sequence from $G$ to $cl (G)$ , [L1] says after each added edge that the graph before the addition is Hamiltonian exactly when the graph after it is Hamiltonian.

L1F1F2

2.1

The sequence is finite, and [L2] identifies its terminal graph with the well-defined closure. Chaining the biconditionals from step 1.1 gives $G$ Hamiltonian if and only if $cl (G)$ is Hamiltonian.

step 1.1F1L2∎

Depends on

Used by

Ore's theorem: an n-vertex graph with n≥3 and deg(u)+deg(v)≥ n for every nonadjacent pair is Hamiltonian Theorem

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

Applied Combinatorics, Eulerian and Hamiltonian Graphs (standard reference, not scraped)