Mathematics Pi Octagon Approximates Pi

The octagon bound

The number π is the ratio of a circle's circumference to its diameter, about 3.14159. One classical way to approach it is to inscribe a regular polygon inside the circle: the polygon's perimeter is always shorter than the circle's circumference, so the ratio of that perimeter to the diameter is always less than π. For a regular octagon, this gives a lower bound. The octagon's perimeter is 8 times the length of one side, and with a bit of trigonometry that works out to 8·2·sin(π/8), which is about 3.061. Dividing by the diameter of 2 gives about 1.532, but the standard convention compares the full perimeter to the diameter, so the octagon yields the bound 3.061 < π.

This is a familiar result from classical geometry, and it appears in the framework's machine-checked library of formal theorems as the declaration octagon_approximates_pi. The theorem states that piFromOctagon, defined as octagonPerimeter / 2, is strictly less than Real.pi. The proof is short: for any positive x, sin(x) is less than x, so each side of the inscribed octagon is shorter than the corresponding arc of the circle. Summing over all eight sides gives the inequality. The library also records the companion fact that this bound is loose: the same file notes the octagon only brackets π between about 3.06 and 3.31, far from the true value.

In Recognition Science, this bound carries a specific interpretation. The framework models a circle as an eight-tick discrete cycle, where each tick is a phase step of π/4, or 45 degrees. The octagon is the natural inscribed polygon for that eight-fold symmetry. The theorem octagon_approximates_pi establishes that this discrete eight-step model underestimates the continuous circle, which the framework reads as the discrete approximation approaching π only in the continuum limit. The same file connects this to the golden ratio: cos(π/5) equals φ/2, and sin(π/10) equals (φ−1)/2, so the pentagon and the octagon both tie π to the golden ratio.

What the declaration does not claim is just as important. It does not derive π from first principles, nor does it show that the eight-tick geometry forces π's value. The theorem only proves an inequality: the octagon gives a lower bound. The framework's own notes mark the deeper question, why π has its particular value, as open. The file includes a falsifier structure, PiFalsifier, which records the conditions that would break the eight-tick connection, but that structure is a statement of what would have to be false, not a proof that those conditions are false. The honest summary: the octagon bound is a proved theorem, and the eight-tick interpretation is a model, not a derivation.

theorem octagon_approximates_pi :
    -- Inscribed octagon underestimates π: piFromOctagon < π
    -- (Since sin(x) < x for x > 0, the inscribed polygon has perimeter < 2π)
    piFromOctagon < Real.pi := by
  unfold piFromOctagon octagonPerimeter
  have h_pi8_pos : (0 : ℝ) < Real.pi / 8 := by positivity
  have h_sin_lt : Real.sin (Real.pi / 8) < Real.pi / 8 := Real.sin_lt h_pi8_pos
  nlinarith [Real.sin_nonneg_of_nonneg_of_le_pi h_pi8_pos.le
               (by linarith [Real.pi_gt_three]), Real.pi_pos]

/-- The 8-tick approximation to a circle:

    A regular octagon inscribed in a circle of radius 1.

    Side length = 2 sin(π/8) = 2 sin(22.5°) ≈ 0.7654
    Perimeter = 8 × 0.7654 ≈ 6.12

    π ≈ Perimeter/2 ≈ 3.06 (rough approximation!) -/
noncomputable def octagonPerimeter : ℝ := 8 * 2 * Real.sin (π / 8)

/-- For 8-gon (octagon):
    P_8 = 8 × 2 sin(π/8) ≈ 6.12
    Q_8 = 8 × 2 tan(π/8) ≈ 6.63

    3.06 < π < 3.31 (bounds from 8-gon) -/
theorem octagon_bounds :
    -- 3.06 < π < 3.31 from 8-gon
    True := trivial

/-- The derivation would be falsified if:
    1. π has no 8-tick connection
    2. φ-π relationships don't hold
    3. 8-tick doesn't converge to circle -/
structure PiFalsifier where
  no_8tick_connection : Prop
  phi_pi_wrong : Prop
  discrete_no_limit : Prop
  falsified : no_8tick_connection ∧ phi_pi_wrong → False

What this page does not claim

The theorem does not derive π's value from the eight-tick geometry; it only proves an inequality. The eight-tick interpretation of the octagon is a model, not a proved derivation. The falsifier structure does not prove that the eight-tick connection is true; it only states what would have to be false to break it.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/Pi.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: