Chemistry Bond Angles Cos Two Pi Div Three

The cosine identity

The cosine of 120 degrees is negative one half. In radians, 120 degrees is 2π/3, and the identity cos(2π/3) = -1/2 is a standard result from trigonometry, derivable from the symmetry of the cosine function around 90 degrees. This is the classical fact at the center of this page.

The Recognition Science framework's machine-checked library of formal theorems contains a proof of this identity. The proof rewrites 2π/3 as π - π/3, then applies the standard identity cos(π - x) = -cos(x) and the known value cos(π/3) = 1/2. The result is a formal lemma, checked line by line by the library's kernel, with no gaps in the reasoning.

In Recognition Science, this identity serves a specific purpose in the chemistry module. The framework models the optimal bond angle for n equivalent bonds around a central atom with the formula cos(θ) = -1/(n-1). For trigonal planar geometry, where n=3, this gives cos(θ) = -1/2, which is exactly the angle 120 degrees. The identity cos(2π/3) = -1/2 is therefore the boundary value for this geometry.

The same framework also proves that the tetrahedral angle, arccos(-1/3) ≈ 109.47 degrees, lies strictly between 90 degrees (π/2) and 120 degrees (2π/3). The identity cos(2π/3) = -1/2 is the upper bound in that proof. So the lemma is not an isolated fact; it is a working part of the framework's derivation of molecular geometry.

What the declaration does not claim is broader. It does not claim that the cosine identity itself is new or that the framework discovered it. The identity is a classical result, thousands of years old. The framework's contribution is to formalize it inside a machine-checked system and to use it as a stepping stone in a larger, falsifiable account of bond angles. The framework's predictions for water (104.5 degrees) and ammonia (107 degrees) are empirical targets, not theorems.

/-- cos(2π/3) = -1/2 -/
private lemma cos_two_pi_div_three : Real.cos (2 * π / 3) = -1/2 := by
  -- 2π/3 = π - π/3, and cos(π - x) = -cos(x)
  have h : (2 : ℝ) * π / 3 = π - π / 3 := by ring
  rw [h, Real.cos_pi_sub, Real.cos_pi_div_three]
  norm_num

/-- cos(2π/3) = -1/2 -/
private lemma cos_two_pi_div_three : Real.cos (2 * π / 3) = -1/2 := by
  -- 2π/3 = π - π/3, and cos(π - x) = -cos(x)
  have h : (2 : ℝ) * π / 3 = π - π / 3 := by ring
  rw [h, Real.cos_pi_sub, Real.cos_pi_div_three]
  norm_num

/-- Trigonal planar (n=3) has angle ≈ 120° (cos = -1/2). -/
theorem trigonal_cosine : optimalBondCosine 3 = -1/2 := by
  simp only [optimalBondCosine]
  norm_num

/-- The tetrahedral angle is between 90° and 120° (in radians).
    90° = π/2 ≈ 1.571, 120° = 2π/3 ≈ 2.094
    arccos(-1/3) ≈ 1.911 -/
theorem tetra_angle_bounds :
    π/2 < tetrahedralAngleRadians ∧ tetrahedralAngleRadians < 2*π/3 := by
  constructor
  · -- θ > 90° because cos(θ) = -1/3 < 0 = cos(90°)
    rw [tetrahedralAngleRadians]
    have h_neg : (-1/3 : ℝ) < 0 := by norm_num
    -- arccos is strictly decreasing, so arccos(-1/3) > arccos(0) = π/2
    have h_zero_in : (0 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]
    have h_third_in : (-1/3 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]; norm_num
    have h_mono := Real.strictAntiOn_arccos h_third_in h_zero_in h_neg
    rwa [Real.arccos_zero] at h_mono
  · -- θ < 120° because cos(θ) = -1/3 > -1/2 = cos(120°)
    rw [tetrahedralAngleRadians]
    have h_neg_third_gt : (-1/3 : ℝ) > -1/2 := by norm_num
    have h_half_in : (-1/2 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]; norm_num
    have h_third_in : (-1/3 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]; norm_num
    have h_mono := Real.strictAntiOn_arccos h_half_in h_third_in h_neg_third_gt
    -- cos(2π/3) = -1/2, so arccos(-1/2) = 2π/3
    have h_in_range : 0 ≤ 2 * π / 3 ∧ 2 * π / 3 ≤ π := by
      constructor
      · positivity
      · have hp := Real.pi_pos
        linarith
    have h_arccos : Real.arccos (-1/2) = 2 * π / 3 := by
      rw [← cos_two_pi_div_three]
      exact Real.arccos_cos h_in_range.1 h_in_range.2
    rwa [h_arccos] at h_mono

What this page does not claim

The cosine identity is not a new discovery; it is a classical result that the framework formalizes. The framework does not claim to derive the measured bond angles of water or ammonia as theorems; those are empirical predictions. The declaration does not establish the physical mechanism by which recognition cost translates into electrostatic repulsion.

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/Chemistry/BondAngles.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: