octagon_bounds
plain-language theorem explainer
Octagon bounds assert that a regular 8-gon supplies the inequality 3.06 < π < 3.31 via its inscribed and circumscribed perimeters. Researchers linking discrete 8-fold symmetry to the emergence of π in Recognition Science cite the result when initializing geometric approximations. The proof is a one-line term that directly asserts the bound statement.
Claim. The perimeters of the inscribed and circumscribed regular octagons on the unit circle satisfy the inequality $3.06 < π < 3.31$.
background
The Mathematics.Pi module targets derivation of π from RS 8-tick geometry, where the 8-tick circle consists of eight discrete phases whose continuous limit yields the circle constant. The fundamental time quantum is the tick τ₀ = 1, with one octave defined as exactly eight ticks. Upstream results supply the tick definition and note that the eight-tick structure is the fundamental evolution period.
proof idea
The proof is a term-mode trivial assertion that directly accepts the stated inequality without calculation or lemma application.
why it matters
The declaration supplies the initial 8-gon bounds inside the MATH-002 development of π from 8-tick geometry. It instantiates the eight-tick octave (T7) from the forcing chain and supplies concrete numerical anchors that later siblings such as piFromOctagon and piSeries can refine. No open questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.