Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-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.

Every closed walk of odd length contains a cycle of odd length

Statement

Every closed walk of odd length in a graph contains, among its traversed edges, a cycle of odd length.

Facts & Assumptions

Given: A finite simple graph and its closed walks.

[F1]

A simple graph has no loop, so an odd closed walk has length at least 3; a closed walk of length m≥3 whose vertices before the repeated endpoint are distinct is a cycle (Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges).

[L1]

Mathematical induction: a property true at 0 and inherited from m to m+1 holds for every natural m (The principle of mathematical induction).

[F2]

If a closed walk (v0,…,vr=v0) has vi=vj with 0≤i<j<r, it splits into closed walks of lengths j−i and r−(j−i); when r is odd, exactly one of these lengths is odd.

Proof

technique · induction
1.1

Let P(m) say that every odd closed walk of length at most m contains an odd cycle. At m=0 there is no odd positive length at most 0, so P(0) holds vacuously.

base
1.2

Fix m and assume P(m). Let W=(v0,…,vr=v0) be an odd closed walk with r≤m+1.

ihgiven
2.1

If r≤m, the inductive hypothesis supplies an odd cycle in W.

step 1.2
2.2

Suppose instead that r=m+1. If v0,…,vr−1 are distinct, then W is itself an odd cycle by [F1].

step 1.2F1
2.3

If those vertices are not distinct, choose 0≤i<j<r with vi=vj. By [F2], W splits into two shorter closed walks, and exactly one has odd length. Its length is at most r−1=m, so P(m) supplies an odd cycle in that subwalk and hence in W.

step 1.2F2choose
3.1

Steps 2.1, 2.2 and 2.3 cover every odd closed walk of length at most m+1, so P(m+1) holds.

step 2.1step 2.2step 2.3
4.1

By [L1], P(m) holds for every natural m. Applying it at the length of any given odd closed walk yields an odd cycle contained in that walk.

step 1.1step 3.1L1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

14 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