pith. sign in
module module high

IndisputableMonolith.Mathematics.Pi

show as:
view Lean formalization →

The Mathematics.Pi module constructs the 8-tick approximation to π from the perimeter of a regular octagon inscribed in the unit circle. It supplies the geometric link between the discrete 8-tick clock and continuous geometry in Recognition Science. The module consists of direct definitions for perimeters and bounds derived from trigonometric evaluations at multiples of π/4.

claimA regular octagon inscribed in the unit circle has side length $2 sin(π/8)$ and perimeter $8 · 2 sin(π/8) ≈ 6.12$, yielding the approximation $π ≈ 3.06$.

background

The module sits inside the Recognition Science framework whose fundamental discrete clock is the 8-tick cycle with phases at 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. It imports the time quantum τ₀ = 1 tick from Constants and the 8-tick structure from EightTick. The supplied doc-comment presents the inscribed octagon as the basic object whose perimeter approximates the circle circumference.

proof idea

This is a definition module, no proofs. It introduces octagonPerimeter, piFromOctagon, inscribedPerimeter, circumscribedPerimeter, octagon_bounds, and related trigonometric identities such as cos(π/5) = φ/2 and sin(π/10) from φ.

why it matters in Recognition Science

The module supplies the geometric content for the eight-tick octave (T7) in the forcing chain. It grounds the transition from discrete ticks to continuous geometry that later supports D = 3 and the derivation of constants. No downstream declarations are listed, indicating it functions as a base layer for higher mathematics in the framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)