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.

Mass growth, stopping, and final-angle claims

PDF p. 27: Proof of Theorem 1.10, stopping cases; PDF p. 28: Proof of Theorem 1.10, stopping cases

Statement

Assume countable choice and use the graph, normalized nonsynchronized stable state, parameters and two-stage construction specified in the construction supplier. In particular, $0 < α \leq 1 / 5$ , $q = 1 + δ > 1$ , $c_{0} = ∣ C_{π / 2} ∣ > 0$ , and $β_{0} = π / 2$ . Here $C_{ψ} = {x \in V : ∣ θ_{x} ∣ \geq ψ}$ uses principal phase representatives $θ_{x} \in (- π, π]$ .

Let $k^{*}$ be the first small-stage index at which either $c_{k} \geq α n$ or $c_{k} \geq q^{k} c_{0} \geq B c_{0} / (2 α)$ , where $B = 1 + c^{+} + α$ . The construction terminates at a finite index $M$ , and $∣ C_{β_{k}} ∣ \geq c_{k}$ for every $0 \leq k \leq M$ . If it stops at $M = k^{*}$ with $c_{M} \geq α n$ , the total angle loss is less than $π / 8$ , $β_{M} > 3 π / 8$ , and $c_{M} \sin^{2} β_{M} > 5 α^{2} n / 2$ . If it continues after $k^{*}$ , it stops with $c_{M} = n / 2$ ; each stage loses less than $π / 8$ , $β_{M} > π / 4$ , and $c_{M} \sin^{2} β_{M} > n / 4 > 5 α^{2} n / 2$ .

Statement references

Two-stage angle and mass construction

Phase tail sets for amplification

The Axiom of Countable Choice (AC_ω)

Facts & Assumptions

[F1]

The construction specifies $a = 1 + c^{-}$ , $B = 1 + c^{+} + α$ , $L = \log (B / (2 α))$ , $δ = a / (2 (c^{+} - c^{-}))$ , $q = 1 + δ$ , $K = ⌈ L / \log q ⌉$ , $- 1 < c^{-} \leq 0 \leq c^{+}$ , $c^{+} > c^{-}$ , and $32 α (1 + 4 c^{+} - 3 c^{-}) L / a^{2} < 1$ . Its small-stage updates, while $k < K$ and $c_{k} < α n$ , are $β_{k + 1} = β_{k} - \arcsin (8 α / a)$ and $c_{k + 1} = \min {q ∣ C_{β_{k}} ∣, α n}$ . If that stage stops below its cap, its large-stage updates are $β_{k + 1} = β_{k} - \arcsin (4 B c_{0} / (a ∣ C_{β_{k}} ∣))$ and $c_{k + 1} = \min {q ∣ C_{β_{k}} ∣, n / 2}$ , stopping at $c_{M} = n / 2$ . These are instructions, not premises asserting their correctness or termination (Two-stage angle and mass construction). The phase tails are defined by the principal representatives in the Statement (Phase tail sets for amplification).

[F2]

Under the graph, stability, normalization and countable-choice hypotheses in the Statement, small-set amplification with $ε = a / 2$ and $ρ = 1$ gives $∣ C_{γ} ∣ \geq \min {q ∣ C_{β} ∣, α n, n / 2}$ whenever $0 < γ < β \leq π / 2$ and $\sin (β - γ) \geq 8 α / a$ (Small-set amplification — Lemma 4.2, The Axiom of Countable Choice (AC_ω)).

[F3]

Under those same hypotheses, large-set amplification with $ε = a / 2$ gives $∣ C_{γ} ∣ \geq \min {q ∣ C_{β} ∣, n / 2}$ whenever $0 < γ < β \leq π / 2$ , $∣ C_{β} ∣ > 0$ , and $\sin (β - γ) \geq 4 B c_{0} / (a ∣ C_{β} ∣)$ (Large-set amplification — Lemma 4.3, The Axiom of Countable Choice (AC_ω)).

[F4]

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

[F5]

The ceiling is the least integer at least its argument. Positive masses satisfying $u_{j + 1} \geq \min {q u_{j}, C}$ with $q > 1$ , $C > 0$ grow at least geometrically before their first cap crossing and reach the cap in finitely many updates. If $u_{j} \geq u_{0} q^{j}$ and decrements satisfy $0 \leq d_{j} \leq b / u_{j}$ on a finite or infinite stage, their total is at most $b q / (u_{0} (q - 1))$ (Geometric growth, truncation and total decrement budgets).

[F6]

The natural logarithm is strictly increasing on positive reals, $\log 1 = 0$ , and $\log (x y) = \log x + \log y$ for $x, y > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F7]

The principal inverse sine satisfies $\sin (\arcsin x) = x$ for $- 1 \leq x \leq 1$ and has values in $[- π / 2, π / 2]$ (Principal inverse sine and inverse cosine). Sine is strictly increasing on $[- π / 2, π / 2]$ (Signs, monotonicity intervals, and ranges of sine and cosine) and is nonnegative on $[0, π]$ (Angular order and elementary inverse-trigonometric bounds).

[F8]

For real $t$ , $\cos (2 t) = \cos^{2} t - \sin^{2} t$ , by the cosine addition formula, and $\cos^{2} t + \sin^{2} t = 1$ ; also $\cos (π / 2) = 0$ and $\sin (- t) = - \sin t$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine, Quarter-turn values and shifts by pi/2 and pi).

[F9]

A property holding at zero and preserved by the successor step holds for every nonnegative integer (The principle of mathematical induction).

Proof

Given: The construction and its hypotheses in the Statement, including $c_{0} > 0$ . Countable choice is retained for the two amplification lemmas; the numerical estimates and deterministic recursion below require no further choices.

Goal: Establish well-defined updates, the tail bounds, finite stopping and the stated final inequalities.

1.1givenF1F4F6algebra

Put $D = 1 + 4 c^{+} - 3 c^{-} = a + 4 (c^{+} - c^{-}) > a > 0$ . Since $α \leq 1 / 5$ and $B \geq 1 + α$ , $B / (2 α) \geq 3$ . Thus $L \geq \log 3 > 1$ , the strict inequality following from [F4] at $x = 2$ . Since $D L / a > 1$ , the hypothesis $32 α D L / a^{2} < 1$ implies $α / a < 1 / 32$ . In particular $0 < 8 α / a < 1 / 4$ , and $δ > 0$ , $q > 1$ , $\log q > 0$ .

1.2F7F8algebra

By [F8], $\cos (2 t) = 1 - 2 \sin^{2} t$ . At $t = π / 4$ , this gives $\sin^{2} (π / 4) = 1 / 2$ . By [F7], for $π / 4 < β \leq π / 2$ , $\sin β > \sin (π / 4) \geq 0$ , hence $\sin^{2} β > 1 / 2$ .

2.1F1F4F5F7F8step 1.1algebra

Write $x = L / \log q > 0$ . If $x \leq 1$ , then $K = 1$ ; if $x > 1$ , the least-integer property gives $K < x + 1 \leq 2 x$ . Also [F4] gives $2 / \log q \leq (2 + δ) / δ = D / a$ . Hence $K \leq \max {1, D L / a}$ . Put $s = \arcsin (8 α / a)$ . By [F4] and [F7], $0 < s \leq 4 π α / a$ ; here $s = 0$ is excluded by $\sin (\arcsin (8 α / a)) = 8 α / a > 0$ and $\sin 0 = 0$ , the latter following from the parity identity in [F8]. Consequently the loss from any at most $K$ small-stage updates is at most $S : = 4 π α K / a < π / 8$ . Indeed, both $32 α / a < 1$ and $32 α D L / a^{2} < 1$ . Thus every proposed small-stage angle is greater than $3 π / 8$ and at most $π / 2$ , before any amplification lemma is invoked.

3.1givenF1F2F5F6F7F9step 1.1step 2.1inductionalgebra

Induct along the small-stage instructions. The initial tail bound is equality by the definition of $c_{0}$ . At each executed update, step 2.1 gives $0 < β_{k + 1} < β_{k} \leq π / 2$ , and [F7] gives $\sin (β_{k} - β_{k + 1}) = 8 α / a$ . Since $0 < ε = a / 2 < a$ and $c^{+} - c^{-} > 0$ , all the hypotheses of [F2] hold. As $α n \leq n / 2$ , it gives $∣ C_{β_{k + 1}} ∣ \geq c_{k + 1}$ . The update and the previous tail bound give $c_{k + 1} \geq \min {q c_{k}, α n}$ , so [F5], applied to each constructed prefix, gives $c_{k} \geq q^{k} c_{0}$ before the cap. The instructions stop this stage at its first cap or at $K$ . By [F6], $q^{k} c_{0} \geq B c_{0} / (2 α)$ is equivalent to $k \log q \geq L$ ; its first integer solution is $K$ . Therefore its stopping index equals the stated $k^{*}$ . If it stops below the cap, $k^{*} = K$ and $c_{k^{*}} \geq q^{K} c_{0} \geq B c_{0} / (2 α) > 0$ . This argument includes a cap already reached at index zero.

4.1F1F3F4F5F7F9step 1.1step 2.1step 3.1inductionalgebra

Suppose the large stage is entered, and write $m = c_{k^{*}}$ , so $0 < m < α n < n / 2$ and $m \geq B c_{0} / (2 α)$ . Set $b = 2 π B c_{0} / a$ and $T = b q / (m δ)$ . Then $T \leq 4 π α q / (a δ) = 4 π α (1 + 2 c^{+} - c^{-}) / a^{2} < π / 8$ , since $1 + 2 c^{+} - c^{-} \leq D$ , $L > 1$ , and $32 α D L / a^{2} < 1$ . Assume inductively that a constructed prefix has the tail bounds and $c_{k^{*} + j} \geq m q^{j}$ at every index before the cap. At its next such index the inverse-sine argument $u_{j} = 4 B c_{0} / (a ∣ C_{β_{k^{*} + j}} ∣)$ is positive and at most $4 B c_{0} / (a m q^{j}) \leq 8 α / a < 1$ . Its decrement $d_{j} = \arcsin u_{j}$ therefore satisfies $0 < d_{j} \leq b / c_{k^{*} + j} \leq (b / m) q^{- j}$ . By [F5], every partial large-stage loss, including this proposed decrement, is at most $T < π / 8$ . Together with step 2.1 this makes the proposed next angle greater than $π / 4$ , so [F3] applies, with its sine condition an equality by [F7]. It supplies the next tail bound and $c_{k^{*} + j + 1} \geq \min {q c_{k^{*} + j}, n / 2}$ , completing the induction. Thus no update fails. The growth-and-cap conclusion in [F5] gives a finite cap crossing; the exact update is at most $n / 2$ , so it stops with $c_{M} = n / 2$ . Both stage losses are strictly less than $π / 8$ , and all angles lie in $(0, π / 2]$ .

4.2givenstep 2.1step 3.1step 1.2algebra

If the construction stops at $M = k^{*}$ with $c_{M} \geq α n$ , step 2.1 gives total loss less than $π / 8$ and $β_{M} > 3 π / 8 > π / 4$ . Therefore $c_{M} \sin^{2} β_{M} > α n / 2 \geq 5 α^{2} n / 2$ , using $0 < α \leq 1 / 5$ . This includes $M = k^{*} = 0$ when the initial cap is already reached.

5.1givenstep 3.1step 4.1step 1.2algebra∎

If the construction continues after $k^{*}$ , step 4.1 gives finite stopping with $c_{M} = n / 2$ , each stage loss less than $π / 8$ , and $β_{M} > π / 4$ . Hence $c_{M} \sin^{2} β_{M} > n / 4$ . Since $5 α^{2} / 2 \leq 1 / 10 < 1 / 4$ and $n > 0$ , $n / 4 > 5 α^{2} n / 2$ . Along with the tail bounds from steps 3.1 and 4.1, this proves every assertion.

Source notes

The critical-step and stopping-case claims are attributed to the cited article. The proof above derives the construction's invariants and angle budgets from the declared mathematical suppliers; the article citation is attribution only.

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. 27–28, proof of Theorem 1.10, critical step and stopping cases