AlgorithmAlgorithm: 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.

Two-stage angle and mass construction

PDF p. 26: Proof of Theorem 1.10, two cases; PDF p. 27: Proof of Theorem 1.10, two cases

Definition

Assume countable choice. Take a finite connected $(n, d^{*}, α, c^{-}, c^{+})$ -expander and a stable, nonsynchronized phase state whose first order parameter is real and nonnegative, as in Angle and mass sequences in the amplification argument and Two-sided spectral expander — Definition 1.9. Thus a stable state is a local minimum of the graph energy, and its first order parameter is the mean of its unit phase vectors. For principal representatives $θ_{x} \in (- π, π]$ , put $C_{ψ} = {x : ∣ θ_{x} ∣ \geq ψ}$ for $0 \leq ψ \leq π$ ; this is the phase tail at angle $ψ$ (Phase tail sets for amplification).

Assume $0 < α \leq 1 / 5$ , $- 1 < c^{-} \leq 0 \leq c^{+}$ , and $c^{+} > c^{-}$ . Put $a = 1 + c^{-}$ , $B = 1 + c^{+} + α$ , $L = \log (B / (2 α))$ , $ε = a / 2$ , $δ = a / (2 (c^{+} - c^{-}))$ , and $q = 1 + δ$ . Here $\log$ is the natural logarithm. Assume the article's condition (1.3): $32 α (1 + 4 c^{+} - 3 c^{-}) L / a^{2} < 1$ . The positive $α$ and nonzero gap make the displayed formulas meaningful.

Set $β_{0} = π / 2$ and $c_{0} = ∣ C_{π / 2} ∣$ . Let $K = ⌈ L / \log q ⌉$ , the least integer at least $L / \log q$ . Starting at $k = 0$ , use the following small-stage update while $k < K$ and $c_{k} < α n$ : $β_{k + 1} = β_{k} - \arcsin (8 α / a)$ and $c_{k + 1} = \min {q ∣ C_{β_{k}} ∣, α n}$ . Let $k_{*}$ be the index at which this stage stops. If $c_{k_{*}} \geq α n$ , stop with $M = k_{*}$ . Otherwise repeatedly use the large-stage update $β_{k + 1} = β_{k} - \arcsin (4 B c_{0} / (a ∣ C_{β_{k}} ∣))$ and $c_{k + 1} = \min {q ∣ C_{β_{k}} ∣, n / 2}$ until $c_{M} = n / 2$ . The inverse sine is its principal real branch. The output is the finite sequence $(β_{k}, c_{k})_{k = 0}^{M}$ .

Facts & Assumptions

[F1]

The sequence definition gives $c_{0} \geq 1$ under the stated graph, normalization, stability, nonsynchronization and countable-choice assumptions. The phase tails are nested as their angle decreases (Angle and mass sequences in the amplification argument, Phase tail sets for amplification, The Axiom of Countable Choice (AC_ω)).

[F2]

For $0 < γ < β \leq π / 2$ , the small-set amplification lemma with $ρ = 1$ gives $∣ C_{γ} ∣ \geq \min {q ∣ C_{β} ∣, α n, n / 2}$ if $\sin (β - γ) \geq 8 α / a$ . The large-set lemma gives $∣ C_{γ} ∣ \geq \min {q ∣ C_{β} ∣, n / 2}$ if $∣ C_{β} ∣ > 0$ and $\sin (β - γ) \geq 4 B c_{0} / (a ∣ C_{β} ∣)$ (Small-set amplification — Lemma 4.2, Large-set amplification — Lemma 4.3).

[F3]

For $0 \leq x \leq 1$ , $\arcsin x \leq π x / 2$ ; for $x \geq 0$ , $\log (1 + x) \geq 2 x / (2 + x)$ , strictly for $x > 0$ (Angular order and elementary inverse-trigonometric bounds).

[F4]

A sequence growing at least by a factor $q > 1$ until a positive cap is reached reaches that cap in finitely many steps. On a geometric stage, decrements bounded by $b / c_{k}$ sum to at most $b q / (c_{k_{*}} (q - 1))$ (Geometric growth, truncation and total decrement budgets). Every real number has an integer part, so the stated ceiling exists (Integer part: for every real x there is exactly one integer m with m ≤ x < m + 1).

[F5]

The principal inverse sine satisfies $\sin (\arcsin x) = x$ for $- 1 \leq x \leq 1$ (Principal inverse sine and inverse cosine). Sine is strictly increasing on $[0, π / 2]$ and $\sin 0 = 0$ (Signs, monotonicity intervals, and ranges of sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi). Together with the nonnegative principal range in [F3], these facts give $\arcsin x > 0$ for $0 < x \leq 1$ .

[F6]

For real $t$ , $\sin^{2} t = (1 - \cos (2 t)) / 2$ , and $\cos (π / 2) = 0$ ; hence $\sin^{2} (π / 4) = 1 / 2$ (Double-angle and quadratic power-reduction identities, Quarter-turn values and shifts by pi/2 and pi).

[F7]

The natural logarithm is strictly increasing on $(0, \infty)$ , satisfies $\log 1 = 0$ and $\log (x y) = \log x + \log y$ for $x, y > 0$ , and obeys $\exp (\log x) = x$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm as the inverse of the exponential function).

[F8]

A property holding at zero and preserved by the successor step holds for every nonnegative integer (The principle of mathematical induction). Here $q^{m}$ for a nonnegative integer $m$ denotes the product of $m$ copies of $q$ , with $q^{0} = 1$ .

Justification

Given: The graph, state and parameters in the definition.

Goal: Show that every executed update is defined, its claimed mass is a tail lower bound, and the procedure stops with a positive final angle. Moreover, show $c_{M} \sin^{2} β_{M} > 5 α^{2} n / 2$ .

1.1 Since $B \geq 1$ and $α \leq 1 / 5$ , $B / (2 α) \geq 5 / 2$ . More sharply, $B / (2 α) \geq 3$ because $B \geq 1 + α$ and $α \leq 1 / 5$ . By logarithm monotonicity in [F7] and the strict bound in [F3] at $x = 2$ , $L \geq \log 3 > 1$ . Also $1 + 4 c^{+} - 3 c^{-} = a + 4 (c^{+} - c^{-}) \geq a > 0$ . Condition (1.3) therefore implies $α / a < 1 / 32$ . In particular $0 < 8 α / a < 1 / 4$ , and $q > 1$ , so $\log q > 0$ by [F7]. [given, F3, F7, algebra]

2.1 Let $D = 1 + 4 c^{+} - 3 c^{-} = a + 4 (c^{+} - c^{-})$ . The ceiling satisfies $K \leq \max {1, 2 L / \log q}$ : if $L / \log q \leq 1$ then $K = 1$ , and otherwise $⌈ x ⌉ \leq 2 x$ for $x \geq 1$ . By [F3], $2 / \log q \leq (2 + δ) / δ = D / a$ . Thus $K \leq \max {1, D L / a}$ . The total decrement of at most $K$ small updates is at most $4 π α K / a < π / 8$ , using [F3], step 1.1 and (1.3). [F3, F4, step 1.1, algebra]

3.1 Verify the updates inductively, as long as they are executed. The small-stage angle remains positive by step 2.1, and its decrement is the positive principal inverse sine of $8 α / a$ . By [F5], $\sin (β_{k} - β_{k + 1}) = 8 α / a$ . Hence [F2] applies, since $ε = a / 2$ , $ρ = 1$ , and $α n \leq n / 2$ . It gives $∣ C_{β_{k + 1}} ∣ \geq c_{k + 1}$ . Before the cap, $c_{k + 1} \geq \min {q c_{k}, α n}$ , so $c_{k} \geq q^{k} c_{0}$ until the cap is reached. If the small stage stops without the cap, it has $k_{*} = K$ . The product law in [F7] and induction [F8] give $\log (q^{m}) = m \log q$ for every nonnegative integer $m$ : the case $m = 0$ uses $\log 1 = 0$ , and multiplying by $q$ adds $\log q$ . Thus $\log (q^{K}) = K \log q \geq L = \log (B / (2 α))$ , so strict logarithm monotonicity and the inverse identity in [F7] give $c_{k_{*}} \geq q^{K} c_{0} \geq e^{L} c_{0} = B c_{0} / (2 α)$ . If the cap is reached, the procedure stops. [F1, F2, F4, F5, F7, F8, step 2.1, induction, algebra]

4.1 In the remaining case, $c_{k_{*}} \geq B c_{0} / (2 α) > 0$ . Before the large-stage cap, induction using [F2] gives $∣ C_{β_{k}} ∣ \geq c_{k} \geq q^{k - k_{*}} c_{k_{*}}$ . Consequently each inverse-sine argument is positive and at most $8 α / a < 1$ . By [F5], each decrement is positive and its sine equals $4 B c_{0} / (a ∣ C_{β_{k}} ∣)$ , as required by [F2]. Also [F3] bounds the total large-stage decrement by $2 π B c_{0} q / (a δ c_{k_{*}}) \leq 4 π α q / (a δ) = 4 π α (1 + 2 c^{+} - c^{-}) / a^{2} < π / 8$ . The last inequality follows from $1 + 2 c^{+} - c^{-} \leq D$ , $L > 1$ , and (1.3). This bound applies to every finite prefix, so the next angle remains positive and the induction is valid at every update. The growth-and-cap assertion in [F4] makes the large stage finite, with $c_{M} = n / 2$ . [F2, F3, F4, F5, F8, step 1.1, step 3.1, induction, algebra]

5.1 The constructed angles strictly decrease and all remain positive. In the small-stage stopping case, step 2.1 gives $β_{M} > 3 π / 8$ and $c_{M} \geq α n$ . By [F5] and [F6], sine is nonnegative and strictly increasing on $[0, π / 2]$ , with $\sin^{2} (π / 4) = 1 / 2$ , so $\sin^{2} (3 π / 8) > 1 / 2$ . Since $α \leq 1 / 5$ , this gives $c_{M} \sin^{2} β_{M} > α n / 2 \geq 5 α^{2} n / 2$ . In the large-stage case, steps 2.1 and 4.1 give $β_{M} > π / 4$ and $c_{M} = n / 2$ , so $c_{M} \sin^{2} β_{M} > n / 4 \geq 5 α^{2} n / 2$ . The mass bounds and strict growth before the relevant cap make the output an amplification sequence. [F1, F3, F5, F6, step 2.1, step 3.1, step 4.1, algebra] ∎

The two update formulas and two-stage stopping construction are attributed to the proof of Theorem 1.10 in Expander graphs are globally synchronizing, PDF pp. 26–28. The local justification uses the declared mathematical suppliers.

Source notes

Depends on

Used by · 2

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–28, proof of Theorem 1.10