ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Period two on a bipartite graph

Example

Let $G = (V, F)$ be an at most countable simple undirected graph that is connected, locally finite, bipartite with $V = V_{0} ⊔ V_{1}$ , and has no isolated vertices. For $x \in V$ , write $N (x) = {y \in V : {x, y} \in F}$ and $\deg (x) = ∣ N (x) ∣$ . Define simple random walk by $p (x, y) = {\begin{cases} 1 / \deg (x), & y \in N (x), \\ 0, & y \notin N (x) . \end{cases}$ Then every vertex has period $d (x) = 2$ .

Facts & Assumptions

Given: The graph and transition matrix $p$ specified above. Local finiteness and the absence of isolated vertices mean $1 \leq \deg (x) < \infty$ for every $x \in V$ .

[F1]

The $n$ -step probabilities satisfy $p^{(n)} (x, y) = K^{n} (x, {y})$ and $p^{(0)} (x, y) = 1_{{x = y}}$ . (Transition matrices and n-step probabilities)

[F2]

For $m, n \geq 0$ , $p^{(m + n)} (x, y) = \sum_{z \in V} p^{(m)} (x, z) p^{(n)} (z, y)$ . (Matrix Chapman–Kolmogorov equations)

[F3]

States communicate when each is accessible from the other, and $x \to y$ means $p^{(n)} (x, y) > 0$ for some $n \in N_{0}$ . (Accessibility, communication, and irreducibility)

[F4]

$R_{x} = {n \in N : n \geq 1, p^{(n)} (x, x) > 0}$ , and, when it is nonempty, $d (x)$ is the greatest positive integer dividing every element of $R_{x}$ . (Period of a state)

[F5]

If $x$ and $y$ communicate, then $d (x) = d (y)$ . (Period is constant on communicating classes)

Proof

Proof technique: use bipartite parity and a two-step backtrack at one vertex, then transfer the period across the connected graph.

1.1given

If $V = \emptyset$ , there is no vertex to check. Otherwise fix $x_{0} \in V$ . Every degree is finite and positive, so the displayed transition probabilities give a stochastic row at each vertex and are positive exactly on graph edges.

2.1F1F2F4step 1.1given

Let $x_{0} \in V_{i}$ . Induction on $n$ using [F1] and [F2] shows that $p^{(n)} (x_{0}, z) > 0$ only for $z \in V_{i}$ when $n$ is even and for $z \in V_{1 - i}$ when $n$ is odd: the base row is the identity row, and in the induction step Chapman–Kolmogorov together with the fact that every positive one-step transition crosses the bipartition flips the support side. Therefore $p^{(n)} (x_{0}, x_{0}) = 0$ for every odd $n \geq 1$ , so every element of $R_{x_{0}}$ is even.

2.2F2F4step 1.1given

Since $x_{0}$ is not isolated, choose a neighbor $z$ . Undirectedness gives $p (x_{0}, z) = 1 / \deg (x_{0}) > 0$ and $p (z, x_{0}) = 1 / \deg (z) > 0$ . The $m = n = 1$ case of [F2] yields $p^{(2)} (x_{0}, x_{0}) \geq p (x_{0}, z) p (z, x_{0}) > 0$ , so $2 \in R_{x_{0}}$ .

3.1F4step 2.1step 2.2given

By [F4], the positive return set at $x_{0}$ contains $2$ and consists only of even integers. Thus $2$ divides every return time, while every common positive divisor must divide the member $2$ ; hence the greatest such divisor is $d (x_{0}) = 2$ .

4.1F1F2F3F5step 3.1given

Fix any $y \in V$ . Connectedness gives a finite edge path $x_{0} = v_{0}, v_{1}, \dots, v_{k} = y$ . If $k \geq 1$ , repeated application of [F2] gives $p^{(k)} (x_{0}, y) \geq \prod_{j = 0}^{k - 1} p (v_{j}, v_{j + 1}) > 0$ ; if $k = 0$ , [F1] gives $p^{(0)} (x_{0}, y) = 1$ . Reversing the path gives positive accessibility from $y$ to $x_{0}$ as well. Thus $x_{0}$ and $y$ communicate by [F3], and [F5] yields $d (y) = d (x_{0}) = 2$ . Since $y$ was arbitrary, every state has period two.

5.1F1F4step 1.1step 2.1step 2.2step 3.1step 4.1given∎

The empty graph has no vertices; a one-vertex graph would have an isolated vertex and is excluded. Degree-one vertices are allowed, and their immediate backtrack still gives a positive two-step return. The zero transitions within each bipartition side force the odd-time vanishing in step 2.1. Period uses positive return times, so the $n = 0$ identity in [F1] does not enter $R_{x}$ ; steps 2.1–3.1 establish the positive-time gcd. The neighbor and path witnesses are used only for each fixed vertex as needed, so the argument uses no choice function or AC. There is no iff claim.

Source notes

LPW §1.3, printed pp. 7–8 (PDF pp. 23–24), defines period using positive return times, proves period invariance for irreducible chains in Lemma 1.6, and explains alternating support classes for a chain of period two; its Example 1.8 uses an even cycle. Section 1.4, printed p. 8 (PDF p. 24), defines simple random walk on an undirected graph by choosing a neighbor uniformly. These finite-chain passages do not prove the general locally finite bipartite-graph claim. The row definition, parity induction, backtrack, and connected-path transfer needed here are made explicit above.

Depends on

Used by

Nothing in the library uses this result yet.

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

Levin, Peres and Wilmer, Markov Chains and Mixing Times, second edition (standard reference, not scraped)