LemmaStatement: AI-adaptedProof: 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.

Parameter and critical-step estimates in general amplification

PDF p. 26: Proof of Theorem 1.10, numerical consequences and critical step; PDF p. 27: Proof of Theorem 1.10, numerical consequences and critical step

Statement

Use the graph, state, parameters and small-stage construction of Two-stage angle and mass construction. In particular, $0 < α \leq 1 / 5$ , $- 1 < c^{-} \leq 0 \leq c^{+}$ , $c^{+} > c^{-}$ , $a = 1 + c^{-}$ , $B = 1 + c^{+} + α$ , $L = \log (B / (2 α))$ , $δ = a / (2 (c^{+} - c^{-}))$ , $q = 1 + δ$ , and $32 α (1 + 4 c^{+} - 3 c^{-}) L / a^{2} < 1$ . The logarithm is natural. Let $c_{0} = ∣ C_{π / 2} ∣ > 0$ , where $C_{β}$ is the phase tail defined in the construction, and let $c_{k}$ be its constructed small-stage mass bounds. Then $L \geq \log 3 > 1$ , $α / a < 1 / 32$ , and $8 α / a < 1$ .

Let $k^{*}$ be the first small-stage index at which either $c_{k} \geq α n$ or both $c_{k} \geq q^{k} c_{0}$ and $q^{k} c_{0} \geq B c_{0} / (2 α)$ . Then $k^{*}$ exists and $k^{*} \leq ⌈ L / \log q ⌉ \leq \max {1, (1 + 4 c^{+} - 3 c^{-}) L / a}$ . The ceiling is the least integer at least its argument.

Facts & Assumptions

[F1]

Under the stated hypotheses, the construction has $c_{0} > 0$ , $L \geq \log 3 > 1$ and $q > 1$ . Before its small-stage cap $α n$ is reached, its mass bounds satisfy $c_{k} \geq q^{k} c_{0}$ ; the construction continues until that cap or index $K = ⌈ L / \log q ⌉$ (Two-stage angle and mass construction).

[F2]

For $x \geq 1$ , $⌈ x ⌉ \leq 2 x$ , and for $x \geq 0$ , $\log (1 + x) \geq 2 x / (2 + x)$ (Elementary angle and logarithm estimates used in amplification).

[F3]

The ceiling exists, and for $q > 1$ the logarithm and geometric growth give $q^{⌈ \log R / \log q ⌉} \geq R$ whenever $R > 1$ (Geometric growth, truncation and total decrement budgets).

Proof

Given: The hypotheses and construction in the Statement.

Goal: Establish the numerical estimates, existence of $k^{*}$ and its stated upper bounds.

1.1givenF1algebra

Set $D = 1 + 4 c^{+} - 3 c^{-} = a + 4 (c^{+} - c^{-})$ . Thus $D \geq a > 0$ . By [F1], $L > 1$ , so the assumed inequality implies $32 α / a < 1$ because $D L / a > 1$ . Consequently $α / a < 1 / 32$ and $8 α / a < 1 / 4 < 1$ . The bound on $L$ is also in [F1].

1.2F1F3algebra

Put $K = ⌈ L / \log q ⌉$ . Since $B / (2 α) = e^{L} > 1$ , [F3] gives $q^{K} c_{0} \geq B c_{0} / (2 α)$ . If the small-stage cap is reached at or before $K$ , the first stopping alternative holds. Otherwise [F1] gives $c_{K} \geq q^{K} c_{0}$ , so the second alternative holds at $K$ . Hence a first such index exists and $k^{*} \leq K$ . This also covers a cap already reached at index zero.

2.1F1F2step 1.2algebra∎

Write $x = L / \log q > 0$ . If $x \leq 1$ , then $⌈ x ⌉ = 1$ . If $x \geq 1$ , [F2] gives $⌈ x ⌉ \leq 2 L / \log q$ . In either case $K \leq \max {1, 2 L / \log q}$ . Also [F2] gives $2 / \log q \leq (2 + δ) / δ$ . Using $δ = a / (2 (c^{+} - c^{-}))$ , the latter ratio equals $(a + 4 (c^{+} - c^{-})) / a = D / a$ . Combining these inequalities with step 1.2 proves the claimed bounds.

The numerical consequences and critical-step estimate are attributed to the proof of Theorem 1.10 in Expander graphs are globally synchronizing, PDF pp. 26–27. The argument above uses the declared suppliers.

Source attribution

Depends on

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. 26–27, proof of Theorem 1.10