circumscribedPerimeter
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove convergence of the sequence to 2π as n tends to infinity.
- Does not embed the specific 8-tick constraint beyond the general n-gon formula.
- Does not derive the numerical value of π.
- Does not invoke the Recognition Composition Law or the phi-ladder.
formal statement (Lean)
82noncomputable def circumscribedPerimeter (n : ℕ) (hn : n ≥ 3) : ℝ :=
proof body
Definition body.
83 n * 2 * Real.tan (π / n)
84
85/-- For 8-gon (octagon):
86 P_8 = 8 × 2 sin(π/8) ≈ 6.12
87 Q_8 = 8 × 2 tan(π/8) ≈ 6.63
88
89 3.06 < π < 3.31 (bounds from 8-gon) -/