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

Elementary properties of the function H

PDF p. 13: Prose before Lemma 2.3; PDF p. 14: Figure 1

Statement

Let $H : (- π, π] \to R$ be the truncated sine-square function: $H (θ) = \sin^{2} (∣ θ ∣)$ for $∣ θ ∣ \leq π / 2$ , and $H (θ) = 1$ for $π / 2 \leq ∣ θ ∣ \leq π$ . Then $H (θ) \geq 0$ and $H (θ) \geq \sin^{2} θ$ for every $θ$ in its domain. On $[0, π]$ , $H$ is nondecreasing, meaning that $H (a) \leq H (b)$ whenever $0 \leq a \leq b \leq π$ , and it is constant on $[π / 2, π]$ .

Statement references

Truncated sine-square function

Facts & Assumptions

[F1]

The two branches in the statement define $H$ on $(- π, π]$ and agree at their overlap (Truncated sine-square function).

[F2]

Sine is strictly increasing on $[- π / 2, π / 2]$ and has range $[- 1, 1]$ (Signs, monotonicity intervals, and ranges of sine and cosine).

[F3]

Sine is nonnegative on $[0, π]$ (Angular order and elementary inverse-trigonometric bounds).

[F4]

Complex sine is defined by $\sin z = (\exp (i z) - \exp (- i z)) / (2 i)$ , so substitution gives $\sin (- z) = - \sin z$ (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential).

Proof

Given: $θ \in (- π, π]$ and $0 \leq a \leq b \leq π$ .

Goal: Prove the nonnegativity, sine-square bound, monotonicity and constancy in the statement.

1.1F1F2F4givenalgebra

If $∣ θ ∣ \leq π / 2$ , [F1] gives $H (θ) = \sin^{2} (∣ θ ∣) = \sin^{2} θ$ ; the second equality follows from [F4], whether $θ$ is nonnegative or negative. If $∣ θ ∣ \geq π / 2$ , [F1] gives $H (θ) = 1 \geq \sin^{2} θ$ , since [F2] gives $∣ \sin θ ∣ \leq 1$ . Both branches are nonnegative, so the first two assertions hold.

2.1F1F2F3givenalgebra∎

If $b \leq π / 2$ , then [F2] and [F3] give $0 \leq \sin a \leq \sin b$ , so $H (a) = \sin^{2} a \leq \sin^{2} b = H (b)$ . If $a \geq π / 2$ , both values are $1$ by [F1]. Otherwise $a \leq π / 2 \leq b$ ; then $H (b) = 1$ and $H (a) = \sin^{2} a \leq 1$ by [F1] and [F2]. Thus $H (a) \leq H (b)$ in every case. The same branch formula gives $H = 1$ throughout $[π / 2, π]$ , completing the proof.

Source attribution

The definition, the comparison with $\sin^{2} θ$ , and the increasing-on- $[0, π]$ assertion are attributed to the article, PDF p. 13; Figure 1 on p. 14 specifies the plotted domain. The proof above is local and uses the stated suppliers.

Depends on

Used by · 4

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 — Abdalla, Bandeira, Kassabov, Souza, Strogatz, Townsend (2026) · PDF p. 13, prose before Lemma 2.3; PDF p. 14, Figure 1