Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13
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.

Every circle has circumference 2 pi r and circumference-to-diameter ratio pi

Statement

For every centre c∈R2 and radius r>0, the once-traversed circle has circumference

C(r)=2πr.

Since its diameter is d(r)=2r, one has C(r)/d(r)=π.

Facts & Assumptions

Given: A centre c∈R2, a real r>0, and the once-around path γ(t)=c+r(cos⁡t,sin⁡t) on [0,2π].

[L1]

Circumference is the length of this once-around path, and diameter is d(r)=2r (Circular arcs, circumference as arc length, and diameter).

[L2]

Vector differentiation is componentwise (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L3]

(sin⁡t)′=cos⁡t, (cos⁡t)′=−sin⁡t, and sin⁡2t+cos⁡2t=1 (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L4]

A C1 path has length equal to the integral of its speed (If γ:[a,b]→Rn is continuous, differentiable on (a,b), and γ′ extends continuously to [a,b], then L(γ)=∫ab∥γ′(t)∥2 dt).

[L5]

The integral of a constant q on [a,b] is q(b−a) (If m≤f≤M on [a,b] then m(b−a)≤L(f,P)≤∫ab‾f≤∫ab‾f≤U(f,P)≤M(b−a) for every partition P; in particular every constant function is integrable, with ∫abc=c(b−a)).

[L6]

Every once-traversed unit semicircle has length π (The arc length of a unit semicircle is pi).

Proof

technique · direct
1.1givenL2L3algebra

By [L2] and [L3], γ′(t)=r(−sin⁡t,cos⁡t) and ∥γ′(t)∥2=r, since r>0.

2.1step 1.1L1L4L5

By [L1], [L4], and [L5], C(r)=L(γ)=∫02πr dt=2πr.

3.1givenstep 2.1L1algebra

Because r>0, the diameter d(r)=2r is nonzero, and step 2.1 gives C(r)/d(r)=(2πr)/(2r)=π.

4.1step 2.1L6algebra∎

At r=1, step 2.1 gives circumference 2π, agreeing with the sum of the two semicircle lengths from [L6].

Depends on

Dependency tree · 2 levels

Sources