octagon_approximates_pi
plain-language theorem explainer
The theorem shows that the perimeter of a regular octagon inscribed in the unit circle, scaled by 1/2, lies strictly below π. Researchers deriving the circle constant from eight-fold discrete symmetry would cite it as the initial lower bound before taking the continuous limit. The argument unfolds the two definitions, invokes the standard inequality sin(x) < x for x > 0, and closes the comparison by linear arithmetic.
Claim. $8 sin(π/8) < π$
background
The module MATH-002 derives π from 8-tick geometry, where the circle constant emerges as the continuous limit of eight discrete phases. octagonPerimeter is defined as the perimeter of the regular octagon inscribed in the unit circle: 8 * 2 * sin(π/8). piFromOctagon is that perimeter divided by 2, yielding the inscribed approximation 8 sin(π/8). Upstream, the definition of octagonPerimeter supplies the explicit trigonometric expression used in the comparison.
proof idea
The tactic proof first unfolds piFromOctagon and octagonPerimeter to reach 8 sin(π/8) < π. It obtains positivity of π/8 by positivity, applies the library fact Real.sin_lt to produce sin(π/8) < π/8, and finishes with nlinarith using sin nonnegativity on [0, π] together with π > 3.
why it matters
The result supplies the strict lower bound required by the 8-tick octave (T7) in the Recognition Science forcing chain before the continuous limit is taken. It directly supports the module target of recovering π from eight-fold symmetry. No downstream declarations are listed, leaving open whether the bound is later combined with circumscribed polygons or series expansions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.