Encyclopedia Mathematics Mathematics Pi

ARTICLE 4 claims 4 theorems

Mathematics Pi

π is the ratio of a circle's circumference to its diameter, about 3.14159, and it appears throughout mathematics and physics.

Verify this page

The constant π

π (pi) is the number you get when you divide a circle's circumference by its diameter. That ratio is the same for every circle, no matter how large or small, and its value is approximately 3.14159. The number is irrational, meaning it cannot be written as a fraction of two whole numbers, and it is transcendental, meaning it is not the solution to any polynomial equation with integer coefficients. The Swiss mathematician Johann Lambert proved irrationality in 1761, and Ferdinand von Lindemann proved transcendence in 1882. π appears far beyond circles: in the normal distribution of statistics, in the formula for angular frequency 2πf, in the reduced Planck constant ħ = h/2π, and in volumes of spheres.

You can compute π by inscribing regular polygons inside a circle and taking the limit as the number of sides grows. An inscribed octagon gives the approximation 8·sin(π/8) ≈ 3.06, which is less than π; a circumscribed octagon gives an upper bound near 3.31. Archimedes used this polygon method around 250 BCE with a 96-gon to bound π between 3.1408 and 3.1429. Later formulas give exact series: the Gregory-Leibniz series π/4 = 1 - 1/3 + 1/5 - 1/7 + ... converges slowly, while the Basel problem π²/6 = 1 + 1/4 + 1/9 + ... ties π to the squares of integers. Machin's formula π/4 = 4·arctan(1/5) - arctan(1/239) was used for centuries to compute digits by hand.

In Recognition Science, the framework models a discrete eight-tick cycle as the fundamental geometric rhythm, and it examines how π emerges from that discreteness. The framework defines an inscribed octagon perimeter and shows it underestimates π, giving the bounds 3.06 < π < 3.31. It also proves a direct connection between π and the golden ratio φ: cos(π/5) = φ/2 and sin(π/10) = (φ - 1)/2. These identities are classical, but the framework highlights them as evidence that the eight-fold symmetry of its discrete cycle carries a natural link to the pentagon and to φ. The framework's library of machine-checked formal theorems records these results, including the transcendence of π, but it does not claim to explain why π has its particular value in a way that differs from standard mathematics.

The honest takeaway is that the framework's π module is a small exploration, not a new derivation. It reuses classical facts: the octagon bounds, the φ identities, the transcendence proof. The framework's own contribution is the perspective that an eight-tick discrete cycle approximates the continuous circle, and that the golden angle 2π/φ² appears naturally in that context. The module does not prove a new value for π, nor does it show that the eight-tick structure forces π to be what it is. It sets up a vocabulary and a falsifier: if one could show the eight-tick connection is false, or that the φ-π link is wrong, the framework's geometric story would fail. For now, the reader can see that π's classical properties stand independently, and the framework's eight-tick geometry offers a suggestive but unproven framing.

THEOREM octagon_approximates_pi · octagon_bounds · IndisputableMonolith/Mathematics/Pi.lean
octagon_approximates_pi · IndisputableMonolith/Mathematics/Pi.lean:59 
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]
octagon_bounds · IndisputableMonolith/Mathematics/Pi.lean:85 
/-- 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
THEOREM cos_pi_5_is_phi_2 · IndisputableMonolith/Mathematics/Pi.lean
cos_pi_5_is_phi_2 · IndisputableMonolith/Mathematics/Pi.lean:122 
/-- π and φ are related through geometry:

    1. **Golden angle**: 2π/φ² ≈ 137.5° (phyllotaxis)
    2. **Pentagon**: Interior angle = 108° = 3π/5
    3. **cos(π/5) = φ/2** (exact!)
    4. **sin(π/10) = (φ-1)/2 = 1/(2φ)** (exact!)

    These connect the circle (π) to the golden ratio (φ). -/
theorem cos_pi_5_is_phi_2 :
    Real.cos (π / 5) = phi / 2 := by
  -- cos(π/5) = (1 + √5)/4 (Mathlib)
  -- φ = (1 + √5)/2, so φ/2 = (1 + √5)/4
  rw [Real.cos_pi_div_five, phi]
  ring
THEOREM sin_pi_10_from_phi · IndisputableMonolith/Mathematics/Pi.lean
sin_pi_10_from_phi · IndisputableMonolith/Mathematics/Pi.lean:137 
theorem sin_pi_10_from_phi :
    Real.sin (π / 10) = (phi - 1) / 2 := by
  -- Use double-angle formula: cos(π/5) = 1 - 2sin²(π/10)
  -- So sin²(π/10) = (1 - cos(π/5))/2
  have h_cos : Real.cos (π / 5) = (1 + Real.sqrt 5) / 4 := Real.cos_pi_div_five
  -- First prove sin²(π/10) = (1 - cos(π/5))/2
  have h_sin_sq : Real.sin (π / 10)^2 = (1 - Real.cos (π / 5)) / 2 := by
    -- Use: cos(2θ) = 1 - 2sin²(θ), so sin²(θ) = (1 - cos(2θ))/2
    -- With θ = π/10, 2θ = π/5
    -- We have cos(π/5) = cos(2·(π/10)) = 1 - 2sin²(π/10)
    have h_cos_double : Real.cos (π / 5) = Real.cos (2 * (π / 10)) := by ring
    rw [h_cos_double]
    -- cos(2x) = 1 - 2sin²(x)
    have h_cos_formula : Real.cos (2 * (π / 10)) = 1 - 2 * Real.sin (π / 10)^2 := by
      -- cos(2x) = 2cos²(x) - 1, but we need 1 - 2sin²(x)
      -- Use Pythagorean: cos²(x) + sin²(x) = 1, so cos²(x) = 1 - sin²(x)
      -- Therefore: cos(2x) = 2(1 - sin²(x)) - 1 = 2 - 2sin²(x) - 1 = 1 - 2sin²(x)
      rw [Real.cos_two_mul]
      have h_pythag : Real.cos (π / 10)^2 + Real.sin (π / 10)^2 = 1 := Real.cos_sq_add_sin_sq (π / 10)
      have h_cos_sq : Real.cos (π / 10)^2 = 1 - Real.sin (π / 10)^2 := by linarith [h_pythag]
      rw [h_cos_sq]
      ring
    rw [h_cos_formula]
    -- Rearrange: 2sin²(π/10) = 1 - cos(π/5), so sin²(π/10) = (1 - cos(π/5))/2
    ring
  -- Now show sin²(π/10) = ((√5 - 1)/4)²
  have h_sq_eq : Real.sin (π / 10)^2 = ((Real.sqrt 5 - 1) / 4)^2 := by
    rw [h_sin_sq, h_cos]
    field_simp
    -- Left: (1 - (1 + √5)/4)/2 = (4 - 1 - √5)/(8) = (3 - √5)/8
    -- Right: ((√5 - 1)/4)² = (5 - 2√5 + 1)/16 = (6 - 2√5)/16 = (3 - √5)/8
    have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
    have hsqrt_sq : (Real.sqrt 5)^2 = 5 := Real.sq_sqrt h5_pos
    -- Expand right side: ((√5 - 1)/4)²
    ring_nf
    -- Now: (3 - √5)/8 = (6 - 2√5)/16
    -- Multiply both sides by 16: 2(3 - √5) = 6 - 2√5
    -- Left: 6 - 2√5, Right: 6 - 2√5 ✓
    field_simp
    ring
    rw [hsqrt_sq]
    ring
  -- Since sin(π/10) > 0 and ((√5 - 1)/4) > 0, we can take square roots
  have h_pos : 0 < Real.sin (π / 10) := Real.sin_pos_of_pos_of_lt_pi (div_pos Real.pi_pos (by norm_num : (0 : ℝ) < 10)) (div_lt_self Real.pi_pos (by norm_num : (1 : ℝ) < 10))
  have h_rhs_pos : 0 < (Real.sqrt 5 - 1) / 4 := by
    have hsqrt5_gt1 : 1 < Real.sqrt 5 := by
      have h : (1 : ℝ)^2 < (5 : ℝ) := by norm_num
      have h1_pos : (0 : ℝ) ≤ 1 := by norm_num
      have h1_sq : Real.sqrt ((1 : ℝ)^2) = 1 := Real.sqrt_sq h1_pos
      rw [← h1_sq]
      exact Real.sqrt_lt_sqrt (by norm_num) h
    linarith
  -- sin(π/10) = (√5 - 1)/4
  -- Since both sides are positive and their squares are equal, they are equal
  have h_eq : Real.sin (π / 10) = (Real.sqrt 5 - 1) / 4 := by
    -- Use: if a² = b², then a = b or a = -b
    have h_or : Real.sin (π / 10) = (Real.sqrt 5 - 1) / 4 ∨ Real.sin (π / 10) = -((Real.sqrt 5 - 1) / 4) := by
      rw [← sq_eq_sq_iff_eq_or_eq_neg]
      exact h_sq_eq
    cases h_or with
    | inl h => exact h
    | inr h =>
      -- If sin(π/10) = -((√5 - 1)/4), this contradicts h_pos since -((√5 - 1)/4) < 0
      linarith [h_pos, h, h_rhs_pos]
  -- Now show (√5 - 1)/4 = (φ - 1)/2
  rw [h_eq, phi]
  -- φ = (1 + √5)/2, so φ - 1 = (1 + √5)/2 - 1 = (√5 - 1)/2
  -- Therefore (φ - 1)/2 = (√5 - 1)/4 ✓
  ring
THEOREM pi_transcendence · IndisputableMonolith/Mathematics/Pi.lean
pi_transcendence · IndisputableMonolith/Mathematics/Pi.lean:268 
/-- Why is π transcendental?

    π is not the root of any polynomial with integer coefficients.

    This means π cannot be constructed with compass and straightedge alone.

    In RS terms: π emerges from the INFINITE limit of 8-tick geometry.
    The discreteness (algebraic) gives way to continuity (transcendental). -/
theorem pi_transcendence :
    -- π is irrational (Lindemann 1882 proved it is actually transcendental,
    -- but irrationality was shown earlier by Lambert in 1761)
    -- Mathlib proves irrationality via the Niven polynomial argument.
    Irrational Real.pi := irrational_pi

What this page does not claim

The framework derives a new value for π. The eight-tick structure forces π to be transcendental. The module proves the golden angle is the fundamental angle of the framework.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND