TheoremStatement: 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 dense bad sets

Statement

Fix a finite $d$ -regular adjacency-slot multigraph on $n \geq 1$ vertices, with normalized adjacency $M$ , and put $α = ∥ M ∣_{1^{⊥}} ∥$ .

Let $α < 1$ and let $B$ be a fixed vertex set of density $δ \in [0, 1]$ . For a walk begun from the uniform distribution and taking $t \geq 0$ steps (thus sampling $t + 1$ vertices), $\Pr [no visit to B] \leq (1 - δ) [1 - (1 - α) δ]^{t} \leq (1 - δ) e^{- (1 - α) δ t} .$ A zeroth power is interpreted as one even when its base is zero.

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

Let $S$ have density $β = ∣ S ∣ / n$ in a finite regular graph and let $P_{S}$ project onto functions supported in $S$ . Then $∥ P_{S} M P_{S} ∥ \leq α + (1 - α) β .$ For a stationary length- $t$ walk, $t \geq 0$ , its confinement probability is $n^{- 1} ⟨ 1_{S}, (P_{S} M P_{S})^{t} 1_{S} ⟩_{0}$ , where the inner product is unnormalized. (Expander walk restricted operator).

Proof

1.1

Apply the confinement identity to $S = V ∖ B$ . The restricted norm is at most $q = α + (1 - α) (1 - δ) = 1 - (1 - α) δ$ . Bounding the matrix power in the unnormalized inner product and using $∥ 1_{S} ∥_{0}^{2} = n (1 - δ)$ gives the first estimate. If $S$ is empty the probability is zero directly.

2.1

For $x \geq 0$ , $1 - x \leq e^{- x}$ : the difference has value zero at zero and derivative $1 - e^{- x} \geq 0$ . Here $x = (1 - α) δ \in [0, 1]$ , so raising this inequality to the nonnegative integer $t$ gives the second bound. At $t = 0$ the probability is $1 - δ$ ; at $δ = 0$ it is one and at $δ = 1$ zero.

step 1.1algebra∎

Depends on

Expander walk restricted operator

Used by

Expander walk hits dense bad sets Example

Dependency tree · two levels

2 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

Hoory–Linial–Wigderson, Expander Graphs and Their Applications, May 2006 draft; §3.2 Theorem3.6 with the sharper Lemma3.8 estimate above, pp28–29. (standard reference, not scraped)