Chemistry Bond Angles Tetra Angle Bounds

The tetrahedral angle

The tetrahedral bond angle is the angle between any two bonds in a molecule with four equivalent bonds arranged around a central atom, such as methane (CH₄). Its value is arccos(-1/3), approximately 109.47 degrees. This number is familiar in chemistry as the angle that minimizes repulsion between four electron pairs on a sphere, and it appears whenever four bonds point to the corners of a regular tetrahedron.

The angle has a long classical history. The tetrahedron itself was studied by the Greeks, and the angle's cosine of -1/3 follows from the geometry of a cube: place a tetrahedron inside a cube so that its vertices are four alternating corners of the cube, and the dot product of two bond vectors gives -1/3. The same value emerges from the VSEPR model of molecular geometry, where four electron pairs around a central atom repel each other into a tetrahedral arrangement. The angle also appears in the dodecahedron, where the golden ratio φ = (1+√5)/2 plays a role in the polyhedron's structure.

The machine-checked declaration tetra_angle_bounds in the framework's library of formal theorems proves a precise inequality: the tetrahedral angle in radians is strictly greater than π/2 (90 degrees) and strictly less than 2π/3 (120 degrees). In plain language, the proof establishes that the angle lies between the right angle and the angle of an equilateral triangle's corner, which matches the known value of about 109.47 degrees. The proof is a theorem in the sense that it is derived from the definition of the angle as arccos(-1/3) using the monotonicity of the cosine function, and it is checked by a machine.

In Recognition Science, the angle is connected to a broader framework. The framework models the optimal bond angle for n equivalent bonds as cos(θ) = -1/(n-1), which gives -1/3 for n=4, the tetrahedral case. The framework also introduces a dimensionless bias proxy, 1 - 1/φ, which is strictly positive and intended to capture a preference for tetrahedral geometry. However, this proxy is a definitional choice, not a derived quantity, and the connection to the golden ratio is a modeling observation rather than a proved consequence.

/-- The tetrahedral cosine is -1/3. -/
theorem tetra_cos_eq : Real.cos tetrahedralAngleRadians = -1/3 := by
  rw [tetrahedralAngleRadians]
  apply Real.cos_arccos
  · norm_num
  · 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

/-- Optimal cosine of bond angle for n equivalent bonds.
    cos(θ_opt) = -1/(n-1) for n ≥ 2. -/
def optimalBondCosine (n : ℕ) : ℝ :=
  if n ≤ 1 then 0 else -1 / (n - 1 : ℝ)

/-- The bias proxy is strictly positive (since φ>1 ⇒ 1/φ<1). -/
theorem angle_bias : 0 < tetra_bias := by
  dsimp [tetra_bias]
  have hφ : 1 < Constants.phi := Constants.one_lt_phi
  have hφpos : 0 < Constants.phi := lt_trans (by norm_num) hφ
  have h_inv_lt : (1 / Constants.phi) < 1 := by
    rw [div_lt_one hφpos]
    exact hφ
  exact sub_pos.mpr h_inv_lt

What this page does not claim

The tetrahedral angle is not derived from the golden ratio; the φ connection is a modeling observation. The framework does not prove that real molecules adopt this angle, only that the geometric definition gives this value. The octahedral formula cos(θ) = -1/5 does not match the observed 90 degrees, and the framework does not claim it does.

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: