ExampleConstruction: AI-adaptedVerification: AI-generated

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.

Published amplification parameters and bounds — Table 1

PDF p. 29: Table 1

Example

Assume countable choice. Let $G = (V, E)$ be a finite connected $d$ -regular $(n, d, α)$ -expander with $n > 0$ and $0 \leq α \leq 0.0816$ . Thus its binary symmetric adjacency matrix $A$ satisfies $∥ A - (d / n) J ∥ \leq α d$ , where $J$ is the all-ones matrix and the norm is the Euclidean operator norm. Let $θ$ be a stable state, meaning a local minimum of the graph energy, with its first order parameter $n^{- 1} \sum_{x \in V} e^{i θ_{x}}$ real and nonnegative. Represent phases in $(- π, π]$ and set $C_{β} = {x \in V : ∣ θ_{x} ∣ \geq β}$ and $r = ∣ C_{π / 2} ∣$ . Suppose $r > 0$ .

All decimals below are exact rationals. Set $a = 2.4093$ , $q = 2.1274$ , $u = \arcsin (0.3272)$ , $c_{i} = a^{i}$ and $β_{i} = π / 2 - i u$ for $0 \leq i \leq 3$ . For $k \geq 0$ , put $c_{3 + k} = a^{3} q^{k}$ and $β_{4 + k} = β_{3 + k} - \arcsin (3.168 / c_{3 + k})$ . The inverse sine is the principal inverse on $[- 1, 1]$ .

The following are simultaneous lower bounds for the exact recurrence values, not instructions to restart the recurrence at rounded entries:

$i$	$0$	$1$	$2$	$3$	$4$	$5$	$\infty$
$β_{i}$	$π / 2$	$1.237$	$0.904$	$0.570$	$0.342$	$0.235$	$0.131$
$c_{i}$	$1.0$	$2.409$	$5.804$	$13.985$	$29.752$	$63.295$	$\infty$

Here the last angle is a lower bound for the limiting angle, while $c_{i} \to \infty$ . In fact every $β_{i}$ exceeds $0.1356$ , so the sequence is also bounded below by $0.132$ . Table 1 attributes the first three transitions to Lemma 4.2 with $ε = 0.23$ and $ρ = 0.38$ , and the later transitions to Lemma 4.3 with $ε = 0.184$ .

For $i = 0, 1, 2$ , the small-set lemma gives $∣ C_{β_{i + 1}} ∣ \geq \min {a ∣ C_{β_{i}} ∣, 0.031 n}$ . For $i \geq 3$ , whenever $∣ C_{β_{i}} ∣ \geq c_{i} r$ , the large-set lemma gives $∣ C_{β_{i + 1}} ∣ \geq \min {q ∣ C_{β_{i}} ∣, n / 2}$ . Consequently, as long as the cap alternative has not occurred, induction gives $∣ C_{β_{i}} ∣ \geq c_{i} r$ . The table records these uncapped lower bounds; it does not assert that an actual finite graph has an infinite phase-tail cardinality.

Facts & Assumptions

[F1]

The phase-tail definition supplies the principal representatives and the displayed sets; the amplification-sequence definition identifies $∣ C_{π / 2} ∣$ as the initial tail mass (Phase tail sets for amplification, Angle and mass sequences in the amplification argument).

[F2]

A regular $(n, d, α_{0})$ -expander is an $(n, d, α_{0}, - α_{0}, α_{0})$ -expander (Regular adjacency expansion supplies two-sided expansion).

[F3]

The small-set and large-set amplification lemmas give their respective minimum bounds under the stated angle, sine, denominator, normalization and countable-choice hypotheses (Small-set amplification — Lemma 4.2, Large-set amplification — Lemma 4.3, The Axiom of Countable Choice (AC_ω)).

[F4]

The exact scalar replay gives the displayed lower bounds, positivity of all recurrence angles, the strict lower bound $0.1356$ , and the parameter comparisons $2 (1 + 0.38) α_{0} / (1 - α_{0} - 0.23) < 0.3272$ , $1 + 0.23 / (2 α_{0}) > a$ , $0.38 α_{0} > 0.031$ , $2 (1 + 2 α_{0}) / (1 - α_{0} - 0.184) < 3.168$ , and $1 + 0.184 / (2 α_{0}) > q$ , where $α_{0} = 0.0816$ (Exact rational replay of the regular amplification constants).

[F5]

A positive geometric sequence with ratio greater than one is unbounded; a recurrence bounded below by geometric growth reaches any positive finite cap (Geometric growth, truncation and total decrement budgets).

Verification

Given: The graph, state, positive initial tail mass and exact scalar recurrences in the example.

Goal: Verify the table bounds and the conditional amplification statements.

1.1givenF2F3F4algebra

Put $α_{0} = 0.0816$ . Since $d$ is a nonnegative degree and $α \leq α_{0}$ , the given adjacency norm bound also holds with $α_{0}$ . By [F2], the graph has two-sided parameters $c^{-} = - α_{0}$ and $c^{+} = α_{0}$ . The denominators in [F4] are positive, $0 < 0.23, 0.184 < 1 - α_{0}$ , and $c^{+} - c^{-} = 2 α_{0} > 0$ . The state is connected and normalized as required by [F3].

2.1givenF1F3F4step 1.1algebrainduction

For the first three transitions, [F4] gives $0 < β_{i + 1} < β_{i} \leq π / 2$ and $\sin (β_{i} - β_{i + 1}) = 0.3272$ above the small-set threshold. Applying [F3] and the comparisons in [F4] yields the stated minimum with $0.031 n$ ; the additional $n / 2$ alternative in the lemma is no smaller than $0.031 n$ . The starting bound is $∣ C_{β_{0}} ∣ = r = c_{0} r$ . If the cap is not attained at a transition, the minimum bound forces the geometric alternative, so induction gives $∣ C_{β_{i}} ∣ \geq c_{i} r$ through the first stage.

2.2givenF3F4step 1.1algebrainduction

For $i \geq 3$ , assume $∣ C_{β_{i}} ∣ \geq c_{i} r > 0$ . The angle difference has sine $3.168 / c_{i}$ , and [F4] bounds the large-set threshold by $3.168 r / ∣ C_{β_{i}} ∣ \leq 3.168 / c_{i}$ . The angle and denominator hypotheses hold by [F4] and positivity of $r$ . Applying [F3] and its growth-factor comparison in [F4] gives the stated minimum. If its $n / 2$ cap is not attained, it gives $∣ C_{β_{i + 1}} ∣ \geq q c_{i} r = c_{i + 1} r$ . Induction continues the lower bound for every uncapped transition.

3.1F1F4F5step 2.2algebra∎

The exact replay [F4] proves each displayed numerical lower bound and the uniform angle bound, including the infinite inverse-sine tail. Since $q > 1$ , [F5] gives $c_{i} \to \infty$ . Thus the last table column describes limiting scalar bounds; on a finite graph the uncapped cardinality inequalities cannot persist indefinitely because every tail is a subset of $V$ . This verifies the example.

Source notes

The table and the stated choices of $ε$ and $ρ$ are attributed to Expander graphs are globally synchronizing, PDF page 29. The exact recurrence and its certified lower bounds are supplied by the independent local scalar replay; the article citation is attribution, not proof of that replay.

Depends on

Used by · 1

Numerical amplification argument for alpha 0.0816

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Expander graphs are globally synchronizing · PDF pp. 29–30, Table 1 and proof of Theorem 1.4