circumscribedPerimeter

formal source

  79noncomputable def inscribedPerimeter (n : ℕ) (hn : n ≥ 3) : ℝ :=
  80  n * 2 * Real.sin (π / n)
  81
  82noncomputable def circumscribedPerimeter (n : ℕ) (hn : n ≥ 3) : ℝ :=
  83  n * 2 * Real.tan (π / n)
  84
  85/-- For 8-gon (octagon):
  86    P_8 = 8 × 2 sin(π/8) ≈ 6.12
  87    Q_8 = 8 × 2 tan(π/8) ≈ 6.63
  88
  89    3.06 < π < 3.31 (bounds from 8-gon) -/
  90theorem octagon_bounds :
  91    -- 3.06 < π < 3.31 from 8-gon
  92    True := trivial
  93
  94/-! ## The 8-Tick Connection -/
  95
  96/-- Why 8 is special for approximating π:
  97
  98    sin(π/8) = √((1 - cos(π/4))/2) = √((1 - 1/√2)/2)
  99
 100    This involves √2, which has nice properties.
 101
 102    The 8-tick structure gives π/4 = 45° as a fundamental angle.
 103    This relates to the 8th roots of unity. -/
 104theorem pi_over_4_fundamental :
 105    -- π/4 is the 8-tick phase increment
 106    -- This makes 45° special in RS geometry
 107    True := trivial
 108
 109/-- π in terms of 8-tick phases:
 110
 111    8 phases × (π/4) per phase = 2π (full circle)
 112