PropositionStatement: 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 hits bad edges

Statement

Let a stationary walk traverse $t \geq 1$ edges of a reverse-paired regular graph with $α < 1$ . For a fixed set $F$ of nonloop bad edges and $ε = ∣ F ∣ / ∣ E ∣$ , $\Pr [at least one bad edge] \geq \frac{t ε}{t ε + 1 + 2 / (1 - α)} .$ For $F = \emptyset$ this lower bound is zero.

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

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$ . (Expander walk bad edge return).

[F2]

For vectors $u, v$ in a real or complex inner product space, $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥ .$ Equality holds if and only if $u$ and $v$ are linearly dependent, including the case in which either vector is zero. (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

Proof

1.1F1

For $ε > 0$ , let $X = \sum_{j = 1}^{t} I_{j}$ count bad edges. Stationarity gives $E X = t ε$ . The return bound gives $E (I_{j} I_{j + i}) \leq ε (ε + α^{i - 1})$ . Hence $E X^{2} \leq t ε + t (t - 1) ε^{2} + 2 t ε \sum_{i = 1}^{t - 1} α^{i - 1} \leq t ε [1 + t ε + 2 / (1 - α)]$ . For $t = 1$ the pair sum is empty.

2.1F2step 1.1∎

On the finite probability space, Cauchy–Schwarz applied to $X$ and the indicator of $X > 0$ yields $(E X)^{2} \leq E X^{2} \Pr [X > 0]$ . Divide by the positive second-moment bound and cancel $t ε$ . If $ε = 0$ , then $X = 0$ and the claimed bound is zero directly, without division.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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 §2.2 Fact2.6, pp9–10, direct consequence. (standard reference, not scraped)