LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Expander walk bad edge return

Statement

Let $F$ be a nonempty set of nonloop ordinary edges of a reverse-paired $d$ -regular graph, and put $ε = ∣ F ∣ / ∣ E ∣$ . In a stationary walk, condition on some edge being in $F$ . For $i \geq 1$ , the probability that the edge $i$ positions later belongs to $F$ is at most $ε + α^{i - 1}$ . Interpret $α^{0} = 1$ .

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

A walk that at each step chooses one of the $d$ ports uniformly has transition matrix $M$ and stationary uniform law $u = 1 / n$ . For any initial probability vector $p$ and integer $t \geq 0$ , using the ordinary Euclidean norm, $∥ M^{t} p - u ∥_{2} \leq α^{t} ∥ p - u ∥_{2}, TV (M^{t} p, u) \leq \frac{\sqrt{n}}{2} α^{t} .$ For $t = 0$ the factor $α^{0}$ is interpreted as one. For $t \geq 1$ , the adjacency-slot power has nontrivial norm $α^{t}$ . Here total variation means half the $ℓ^{1}$ distance. (Expander walk contraction).

Proof

1.1

The conditioned edge is uniform in $F$ and its orientation is uniform. Its terminal vertex therefore has law $x_{v} = \deg_{F} (v) / (2 ∣ F ∣)$ . The next-step probability of using $F$ from $v$ is $y_{v} = \deg_{F} (v) / d = (2 ∣ F ∣ / d) x_{v}$ . Also $\max x_{v} \leq d / (2 ∣ F ∣)$ and $\sum x_{v} = 1$ , whence $∥ x ∥_{2}^{2} \leq d / (2 ∣ F ∣)$ . This conditioning is legitimate because $F \neq \emptyset$ .

F1algebra

2.1

Between that terminal vertex and the later tested edge there are $i - 1$ transitions, so the probability is $y^{T} M^{i - 1} x$ . Its constant part is $y^{T} u = 2 ∣ F ∣ / (d n) = ε$ . For the other part, spectral contraction and Cauchy–Schwarz give absolute value at most $(2 ∣ F ∣ / d) ∥ x - u ∥_{2}^{2} α^{i - 1} \leq α^{i - 1}$ ; here $y = (2 ∣ F ∣ / d) x$ allows its constant component to be removed in that inner product. This proves the result, including adjacent edges $i = 1$ . The nonloop condition ensures the stated two-endpoint count.

F1step 1.1algebra∎

Depends on

Expander walk contraction

Used by

Expander walk hits bad edges Proposition

Dependency tree · two levels

3 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

Irit Dinur, The PCP theorem by gap amplification; §2.1 Proposition2.5 and its full proof, pp9–10. (standard reference, not scraped)