octagonPerimeter
plain-language theorem explainer
octagonPerimeter supplies the perimeter of a regular octagon inscribed in the unit circle as 16 sin(π/8). Researchers deriving π from discrete 8-fold symmetry in Recognition Science cite this as the base geometric object for the 8-tick bound. The declaration is introduced directly as a noncomputable real expression using the chord-length formula.
Claim. The perimeter of a regular octagon inscribed in the unit circle equals $16 sin(π/8)$.
background
The Mathematics.Pi module targets derivation of π from RS 8-tick geometry, where the circle is treated as the continuous limit of 8 discrete phases. The supplied doc-comment states that each side has length 2 sin(π/8) ≈ 0.7654, so the perimeter is approximately 6.12 and yields a rough π estimate of 3.06 when divided by 2. This definition rests on the EightTick import that encodes the 8-fold symmetry from the T7 eight-tick octave in the forcing chain.
proof idea
The declaration is a direct definition that applies the standard chord-length formula: central angle π/8 gives side length 2 sin(π/8), and multiplication by 8 produces the perimeter.
why it matters
This definition anchors the 8-tick approximation sequence in the Recognition Science framework. It is invoked by piFromOctagon (which divides the perimeter by 2) and by the theorem octagon_approximates_pi (which proves the inscribed perimeter lies below 2π). The construction aligns with the T7 eight-tick octave landmark that forces D = 3 spatial dimensions and supplies the discrete starting point for the module's question on why π takes its observed value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.