TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi

Statement

For every natural $n \geq 3$ , let $I_{n}$ and $O_{n}$ be the perimeters of the regular $n$ -gons respectively inscribed in and circumscribed about the unit circle. Then

$I_{n} = 2 n \sin (π / n), O_{n} = 2 n \tan (π / n),$

$I_{n} < 2 π < O_{n} .$

The sequence $(I_{n})_{n \geq 3}$ is strictly increasing, $(O_{n})_{n \geq 3}$ is strictly decreasing, and both converge to $2 π$ , the circumference of the unit circle.

Facts & Assumptions

Given: A natural $n \geq 3$ , the regular inscribed and circumscribed $n$ -gons of the statement, and the functions $f (x) = \sin x / x$ and $g (x) = \tan x / x$ on $(0, π / 2)$ .

[L1]

The addition formulas hold for sine and cosine, and $\sin^{2} x + \cos^{2} x = 1$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[L2]

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

[L3]

Tangent is $\sin x / \cos x$ and secant is $1 / \cos x$ on their natural domains; there $(\tan x)^{'} = \sec^{2} x$ and $(\sec x)^{'} = \sec x \tan x$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant).

[L4]

$(\sin x)^{'} = \cos x$ , $(\cos x)^{'} = - \sin x$ , $\sin 0 = 0$ , and $\cos 0 = 1$ ; sums, products, and quotients obey the usual derivative rules on their natural domains (The derivatives of sine and cosine are cosine and minus sine, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L5]

Differentiability implies continuity. On an interval, a continuous function with positive derivative at every interior point is strictly increasing, and one with negative derivative at every interior point is strictly decreasing (A function differentiable at $c$ is continuous at $c$ , On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed).

[L6]

$\lim_{x \to 0} \sin x / x = 1$ (The limit of sin x divided by x at zero is one).

[L7]

Sums, products, and quotients of convergent real sequences have the corresponding limits when the limiting denominator is nonzero (Algebra of limits: sums, scalar multiples, products and quotients).

[L8]

The length of a path is the supremum of its polygonal lengths, and refinement cannot decrease polygonal length (Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability, Refining a partition cannot decrease its inscribed polygonal length).

[L9]

The unit-circle circumference is $2 π$ (Circular arcs, circumference as arc length, and diameter, Every circle has circumference 2 pi r and circumference-to-diameter ratio pi).

[L10]

The Euclidean norm is induced by the sum of coordinate squares, and natural numbers in real formulas are the canonical naturals of the field (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L11]

The constant $π$ is positive and $π / 2$ is the least positive zero of cosine (Pi as twice the smallest positive zero of cosine).

[L12]

For every $ε > 0$ there is a natural $N \geq 1$ with $1 / N < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · direct

1.1

Since $n \geq 3$ and [L11] gives $π > 0$ , one has $0 < π / n < π / 2$ . By [L2] and [L4], both $\sin (π / n)$ and $\cos (π / n)$ are positive. Adjacent vertices of the inscribed polygon subtend angle $2 π / n$ ; using [L1] and [L10], their squared distance is $2 - 2 \cos (2 π / n) = 4 \sin^{2} (π / n)$ , so the side length is $2 \sin (π / n)$ and $I_{n} = 2 n \sin (π / n)$ .

givenL1L2L4L10L11algebra

1.2

By [L12], $π / n \to 0$ as $n \to \infty$ ; [L6] gives $f (π / n) \to 1$ . Also $\cos (π / n) \to 1$ by [L4] and [L5], so $g (π / n) = f (π / n) / \cos (π / n) \to 1$ by [L7].

L4L5L6L7L12

1.3

The derivative of $f$ has the sign of $x \cos x - \sin x$ . The function $h (x) = \sin x - x \cos x$ has derivative $x \sin x > 0$ on $(0, π / 2)$ by [L2] and [L4], and tends to $0$ at $0$ by [L4]. Hence $h (x) > 0$ , $f^{'} (x) < 0$ , and $f$ is strictly decreasing by [L5].

L2L4L5algebra

1.4

The derivative of $g$ has the sign of $k (x) = x \sec^{2} x - \tan x$ . From [L2] to [L4], $k^{'} (x) = 2 x \sec^{2} x \tan x > 0$ on $(0, π / 2)$ . Moreover, [L3], [L4], [L6], and [L7] give $k (x) \to 0$ as $x \to 0$ . Thus $g^{'} (x) > 0$ , so $g$ is strictly increasing by [L5].

L2L3L4L5L6L7algebra

2.1

The two tangent lines at adjacent vertices meet on the angle bisector. The resulting right triangle has adjacent side $1$ , opposite side half a polygon side, and angle $π / n$ ; by step 1.1 and [L3] its half-side is $\tan (π / n)$ , so $O_{n} = 2 n \tan (π / n)$ .

givenstep 1.1L3algebra

2.2

The inscribed edges form a polygonal approximation to the once-around circle, so [L8] and [L9] give $I_{n} \leq 2 π$ . By [L2] and [L4], $1 - \cos x > 0$ for $0 < x < π / 2$ ; hence [L4] and [L5] applied to $x - \sin x$ give $\sin x < x$ there and $I_{n} < 2 π$ .

step 1.1L2L4L5L8L9algebra

2.3

Since $n \mapsto π / n$ is strictly decreasing for $n \geq 3$ , step 1.3 gives $I_{n} = 2 π f (π / n) < 2 π f (π / (n + 1)) = I_{n + 1}$ .

step 1.1step 1.3algebra

3.1

The derivative of $\tan x - x$ is $\sec^{2} x - 1 = \tan^{2} x > 0$ on $(0, π / 2)$ by [L2] to [L5]. Thus $\tan x > x$ there, and step 2.1 gives $O_{n} > 2 π$ .

step 2.1L2L3L4L5algebra

3.2

Since $n \mapsto π / n$ decreases, step 1.4 gives $O_{n + 1} = 2 π g (π / (n + 1)) < 2 π g (π / n) = O_{n}$ .

step 2.1step 1.4algebra

4.1

Therefore $I_{n} = 2 π f (π / n) \to 2 π$ and $O_{n} = 2 π g (π / n) \to 2 π$ by [L7]. Together with [L9], the common limit is exactly the unit-circle circumference.

step 1.1step 2.1step 1.2L7L9∎

Depends on

Used by

The zero, period, arc-length, polygonal, area, circumference, series, and product characterizations all give the same pi Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 193 results over 35 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Rutgers Mathematics 373, Workshop 9 Solutions: Pi and the AGM (standard reference, not scraped)
J. Lebl, Basic Analysis II, section 11.4.3 (standard reference, not scraped)