Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21
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.

The arc length of one sine period is 42 E(1/2)

Example

For 0<k<1, write

E(k):=∫0π/21−k2sin⁡2t dt

for the complete elliptic integral of the second kind. The graph of sine over one period, parametrized by γ(x)=(x,sin⁡x) for 0≤x≤2π, has arc length

L(γ)=42 E(1/2).

Facts & Assumptions

Given: The graph path γ(x)=(x,sin⁡x) on [0,2π].

[L1]
[L2]

(sin⁡x)′=cos⁡x on R (The derivatives of sine and cosine are cosine and minus sine).

[L3]

The supplementary, reflection, and quarter-turn identities give cos⁡(π−x)=−cos⁡x, cos⁡(π/2−x)=sin⁡x, and cos⁡(−x)=cos⁡x (Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions).

[L6]

Every positive real has a unique positive square root (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a, case n=2).

[L7]

Differentiable real functions are continuous (A function differentiable at c is continuous at c).

[L8]

The number π=2γ is positive because the smallest positive zero of cosine satisfies γ∈(0,2) (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two).

[L9]

For α∈R, the function u↦uα is continuous on (0,∞); in particular the positive square-root function is continuous there (Continuity and derivatives of positive-base real powers).

Verification

technique · direct
1.1L2L5L7L8L9L10algebra

If 0<k<1, then [L5] gives 1−k2sin⁡2t≥1−k2>0. By [L2], [L7], [L9], and [L10], the integrand defining E(k) is continuous on [0,π/2] and therefore integrable. Thus E(k) is well defined on the stated range.

1.2L1L2L7L8

The derivative in [L2] is continuous by [L7], and [L8] gives 0<2π, so [L1] gives L(γ)=∫02π1+cos⁡2x dx.

2.1step 1.2L3L4

Split the integral in step 1.2 at π/2, π, and 3π/2. The affine reflections and translations licensed by [L4], together with [L3] and the square on cosine, show that all four pieces equal ∫0π/21+cos⁡2x dx.

3.1step 2.1L5L6constructalgebra

The modulus k:=1/2 exists by [L6] and satisfies 0<k<1. By [L5], 1+cos⁡2x=2−sin⁡2x=2(1−12sin⁡2x), so the quarter-period integral in step 2.1 is 2 E(1/2).

4.1step 2.1step 3.1algebra∎

Multiplying the quarter-period value in step 3.1 by the symmetry factor in step 2.1 yields L(γ)=42 E(1/2).

Depends on

Used by

Dependency tree · two levels

87 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources