inscribedPerimeter
plain-language theorem explainer
The definition supplies the perimeter of a regular n-gon inscribed in the unit circle as 2n sin(π/n) for integer n at least 3. Workers on Archimedean bounds or discrete-to-continuous limits in Recognition Science cite this expression when constructing squeeze theorems for π. It is introduced by direct substitution of the chord-length formula with no additional lemmas.
Claim. For each integer $n$ with $n$ at least 3, the perimeter of the regular $n$-gon inscribed in the unit circle equals $2n$ times the sine of $π$ divided by $n$.
background
The Mathematics.Pi module derives π from 8-tick geometry in Recognition Science. The 8-tick circle consists of eight discrete phases whose continuous limit yields the observed value of π. The inscribed-perimeter definition implements one half of Archimedes' classical squeeze: the perimeter $P_n$ of the inscribed $n$-gon satisfies $P_n/2 < π < Q_n/2$, where $Q_n$ is the corresponding circumscribed perimeter.
proof idea
One-line definition that directly encodes the chord length 2 sin(π/n) for each of the n sides of the unit-circle polygon.
why it matters
The definition supplies the lower bound for the Archimedean approximation sequence and feeds the sibling results piFromOctagon and octagon_bounds. It instantiates the eight-tick octave (T7) by taking the n-gon limit of the discrete 8-fold symmetry. The module leaves open whether this geometric origin explains the specific transcendental value of π beyond its known series representations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.