The trigonometric constants

cos(2πk/15) and sin(2πk/15) are within 2⁻⁷⁰ of the checker's tables. For k = 1 this follows from the closed form 2π/15 = π/3 − π/5 with cos(π/5) = (1 + √5)/4; the other multiples follow by complex multiplication, tracking the error exactly in ℚ.

theorem Cayley.sqrt5_bounds : 2.2360679774997896964091736687312762 ≤ √5 ∧ √5 ≤ 2.2360679774997896964091736687312763

theorem Cayley.sqrt3_bounds : 1.7320508075688772935274463415058723 ≤ √3 ∧ √3 ≤ 1.7320508075688772935274463415058724

theorem Cayley.sin_pi_div_five_bounds : 0.5877852522924731291687059546390 ≤ Real.sin (Real.pi / 5) ∧ Real.sin (Real.pi / 5) ≤ 0.5877852522924731291687059546391

noncomputable def Cayley.θ₁ : ℝ

θ₁ = 2π/15.

Equations

• Cayley.θ₁ = 2 * Real.pi / 15

theorem Cayley.θ₁_eq : θ₁ = Real.pi / 3 - Real.pi / 5

theorem Cayley.cos_θ₁_bounds : 0.9135454576426008955021275719 ≤ Real.cos θ₁ ∧ Real.cos θ₁ ≤ 0.9135454576426008955021275720

theorem Cayley.sin_θ₁_bounds : 0.4067366430758002077539859903 ≤ Real.sin θ₁ ∧ Real.sin θ₁ ≤ 0.4067366430758002077539859904

theorem Cayley.sin_θ₁_le_wedge : Real.sin θ₁ ≤ 57 / 128 * Real.cos θ₁

The wedge slope bounds the tangent.

theorem Cayley.cos_θ₁_pos : 0 < Real.cos θ₁