ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-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.

Random walk on a finite undirected graph is reversible

Example

Let $G = (V, E)$ be a finite connected undirected simple graph with at least one edge (A finite simple graph is a finite vertex set together with a set of two-element vertex subsets). Simple random walk on $G$ has

$P (v, w) = {\begin{cases} \frac{1}{\deg_{G} (v)}, & {v, w} \in E, \\ 0, & otherwise, \end{cases}$

and $π (v) = \deg_{G} (v) / (2 ∣ E ∣)$ is a reversible probability distribution for $P$ , hence invariant (Reversible measure and detailed balance, Detailed balance implies invariance).

Facts & Assumptions

Given: A finite connected simple graph $G = (V, E)$ with $∣ E ∣ \geq 1$ , the degree function $\deg_{G}$ , and the displayed walk $P$ .

[F1]

A finite simple graph is an ordered pair $(V, E)$ with $V$ finite and $E \subseteq [V]^{2} = {{u, v} \subseteq V : u \neq v}$ ; every edge has two distinct endpoints and there are no loops. (A finite simple graph is a finite vertex set together with a set of two-element vertex subsets)

[F2]

Distinct vertices $u, v$ are adjacent when ${u, v} \in E$ ; $N_{G} (v) = {u \in V : {u, v} \in E}$ is the open neighbourhood and $\deg_{G} (v) = ∣ N_{G} (v) ∣$ the degree. (Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree)

[F3]

For every finite simple graph, $\sum_{v \in V} \deg_{G} (v) = 2 ∣ E ∣$ . (Handshake lemma: the sum of the vertex degrees is twice the number of edges)

[F4]

A state measure $μ : E \to [0, + \infty)$ with $μ (x) < + \infty$ satisfies detailed balance for $p$ when $μ (x) p (x, y) = μ (y) p (y, x)$ for all $x, y$ ; it is a reversible probability distribution when additionally $\sum_{x} μ (x) = 1$ . (Reversible measure and detailed balance)

[F5]

Any finite-point-mass nonnegative measure satisfying detailed balance for a countable transition matrix satisfies $μ p = μ$ ; a reversible probability distribution is therefore invariant. (Detailed balance implies invariance)

[F6]

A graph is connected when its vertex set is nonempty and every two vertices are joined by a path, equivalently a walk. Its connected component is the induced subgraph on the vertices reachable from a given vertex. (Connected graphs and connected components defined by the existence of vertex paths)

Verification

Given: A finite connected simple graph $G = (V, E)$ with $∣ E ∣ \geq 1$ and the walk $P (v, w) = 1 / \deg_{G} (v)$ on edges with no loops.

Proof technique: check positivity of the degrees, normalize the degree measure by the handshake lemma, verify detailed balance on edges and nonedges, and invoke the general detailed-balance lemma.

1.1F1F2F6given

Every vertex has $\deg_{G} (v) \geq 1$ : if some $v$ had $\deg_{G} (v) = 0$ then, by [F2], $v$ is adjacent to no vertex; if $∣ V ∣ = 1$ then $E = \emptyset$ by [F1], contradicting $∣ E ∣ \geq 1$ , and if $∣ V ∣ \geq 2$ then $v$ cannot be joined to any other vertex by a walk, contradicting connectedness. Hence $P$ is well defined and $P (v, w) \geq 0$ for all $v, w$ .

2.1F1F2step 1.1given

The rows of $P$ sum to one: $\sum_{w \in V} P (v, w) = ∣ N_{G} (v) ∣ / \deg_{G} (v) = 1$ for every $v$ , since the only nonzero entries are over the neighbors and $P (v, v) = 0$ because there are no loops; thus $P$ is a transition matrix.

2.2F3step 1.1given

The measure $π (v) : = \deg_{G} (v) / (2 ∣ E ∣)$ is a probability vector: it is nonnegative, $\sum_{v \in V} π (v) = \frac{1}{2 ∣ E ∣} \sum_{v} \deg_{G} (v) = 1$ by [F3], and $2 ∣ E ∣ \geq 2 > 0$ ; moreover $π (v) > 0$ for every $v$ by step 1.1, so $π$ is finite-valued on the finite set $V$ .

3.1F2step 2.2algebra

Detailed balance holds. If ${v, w} \in E$ then $π (v) P (v, w) = \frac{\deg_{G} (v)}{2 ∣ E ∣} \cdot \frac{1}{\deg_{G} (v)} = \frac{1}{2 ∣ E ∣}$ and likewise $π (w) P (w, v) = \frac{1}{2 ∣ E ∣}$ , using $\deg_{G} (v), \deg_{G} (w) > 0$ ; if $v \neq w$ and ${v, w} \notin E$ then $P (v, w) = P (w, v) = 0$ so both sides vanish; and for $v = w$ both sides are $π (v) P (v, v) = 0$ since $P (v, v) = 0$ .

4.1F4F5step 3.1given

By [F4] the identity of step 3.1 makes $π$ a reversible probability distribution for $P$ , and [F5] then gives $π P = π$ , so $π$ is invariant.

5.1F3F4F6step 1.1step 4.1given∎

Boundary and scope cases: the one-vertex edgeless graph is excluded because then $∣ E ∣ = 0$ , the normalizer $2 ∣ E ∣$ vanishes and the displayed transition row would divide by the degree $0$ ; a graph with several connected components is not covered by the connectivity hypothesis, although the same computation applies to each component containing an edge, with its own positive degree normalizer. An isolated-vertex component has degree zero, so neither displayed formula defines a walk or probability there; a separate absorbing-row convention would give its point mass as a reversible law; the walk has no holding probability, so $P (v, v) = 0$ and the diagonal detailed-balance identity is $0 = 0$ ; irreducibility of the walk follows from connectedness but is not needed for reversibility; and no choice principle is used, all objects being determined by the finite graph.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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–Wilmer, Markov Chains and Mixing Times, second edition, §1.4 and Example 1.12, printed pp. 8–10 / PDF pp. 24–26 (standard reference, not scraped)