What is π, actually?

The school definition of π is the ratio of a circle's circumference to its diameter, about $3.14159$. As a definition this assumes two things. It assumes a circle's boundary has a length, which is a real claim about a curved object and needs a proof. And it assumes the ratio comes out the same for every circle, large or small, which needs a proof too. Until both are proved, "the ratio" does not name a number.

A definition with no circle in it

Sine and cosine are defined by their power series (Sine and cosine defined by their real power series), with no triangles and no angles: two functions built from series that converge at every real number. Cosine starts at $\cos 0=1$, and the library proves it has a smallest positive zero, lying strictly between $0$ and $2$ (Cosine has a smallest positive zero, lying strictly between zero and two). π is defined as twice that zero (Pi as twice the smallest positive zero of cosine).

That is the whole definition. It names one specific real number, it presupposes nothing about circles or lengths, and every ingredient in it is proved.

Earning the circle back

A definition is a choice, and this one must agree with what everyone means by π. The library defines the circumference of a circle as the arc length of the curve tracing it (Circular arcs, circumference as arc length, and diameter) and proves that for every centre and every radius $r$ the circumference is $2\pi r$ (Every circle has circumference 2 pi r and circumference-to-diameter ratio pi). Divide by the diameter $2r$: the ratio is π, the same number for every circle. The school definition comes back as a theorem, with both of its hidden assumptions proved on the way.

One number, many doors

π is over-determined. The library keeps a ledger proving nine further characterizations give the same constant (The zero, period, arc-length, polygonal, area, circumference, series, and product characterizations all give the same pi): the first positive zero of sine (Pi is the first positive zero of sine), half the least common period of sine and cosine (Pi is equivalently the first sine zero, twice the first cosine zero, and half the least common period), the length of a unit semicircle (The arc length of a unit semicircle is pi), the area of the unit disc (A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi), the limit of Archimedes' inscribed and circumscribed polygon perimeters (Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi), and series and product formulas besides. Any of them could serve as the definition; the library takes the cosine zero and proves the rest agree.

One assumption left

"Circumference" leaned on a phrase this article never examined: the arc length of a curve. A circle is curved, a ruler is straight, and it is not obvious that a curved line has a length at all. Some curves have none (The Koch curve is a uniform limit of polygonal paths of lengths $(4\mathrm{/}3{)}^n$ but is not rectifiable). That is the next part of this rabbit hole: how long is a curve?