circumscribedPerimeter
plain-language theorem explainer
The definition supplies the perimeter of a regular n-gon circumscribed about the unit circle as 2n tan(π/n) for integer n at least 3. Researchers deriving π from discrete 8-fold symmetry in Recognition Science cite it to obtain the upper bound in polygon approximations. The expression follows at once from the tangent length of each central isosceles triangle.
Claim. For each integer $n ≥ 3$, the circumscribed perimeter is defined by $P_n = 2n tan(π/n)$.
background
The Mathematics.Pi module targets derivation of π from RS 8-tick geometry, where the circle constant emerges as the continuous limit of eight discrete phases under eight-fold symmetry. This definition provides the explicit upper-bound formula for regular polygons. The upstream theorem from PrimitiveDistinction reduces seven independent axioms to four substantive structural conditions plus three definitional facts, supplying the axiomatic base for introducing geometric quantities such as perimeters.
proof idea
One-line definition that directly applies the tangent of the central angle π/n to each of the n sides of the circumscribed polygon.
why it matters
The definition fills the upper-bound slot in the 8-tick geometric chain (T7) that recovers π inside Recognition Science. It pairs with the inscribed-perimeter sibling to produce concrete bounds such as the octagon case 3.06 < π < 3.31 shown in the module comment. Downstream siblings including piFromOctagon and octagon_bounds apply it to close the derivation; the module leaves open whether the eight-tick discreteness selects the observed numerical value beyond the standard limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.