Encyclopedia Chemistry Chemistry Bond Angles Tetrahedral Cosine

ARTICLE 4 claims 3 theorems 1 model

Chemistry Bond Angles Tetrahedral Cosine

The tetrahedral bond angle, 109.47 degrees, is the angle whose cosine is exactly -1/3, and a machine-checked library proves that value follows from a general formula.

The tetrahedral cosine

The tetrahedral bond angle is the angle between any two bonds in a molecule where a central atom is surrounded by four identical substituents, as in methane (CH₄). Its value is approximately 109.47 degrees, and it is exactly the angle whose cosine is -1/3. This number is not arbitrary: it is the angle that places four points on a sphere as far apart from one another as possible, which is the geometry that minimizes electrostatic repulsion between electron pairs around the central atom.

The general pattern for n equivalent bonds around a central atom is cos(θ) = -1/(n-1). For two bonds this gives cos(θ) = -1, an angle of 180 degrees, a straight line. For three bonds it gives cos(θ) = -1/2, an angle of 120 degrees, the trigonal planar geometry. For four bonds it gives cos(θ) = -1/3, the tetrahedral angle. For six bonds the formula gives cos(θ) = -1/5, but the observed octahedral geometry uses 90 degrees, so the formula does not extend to all coordination numbers.

The formula cos(θ) = -1/(n-1) is a definitional choice in the Recognition Science framework, not a derived physical law. The framework defines a quantity called optimalBondCosine that encodes this formula, and its machine-checked library of formal theorems proves that for n = 4 the value is -1/3. That proof is a theorem: it derives the cosine value from the definition. The library also proves that the angle lies between 90 and 120 degrees, and that the cosine of the angle is indeed -1/3.

In Recognition Science, the tetrahedral angle is connected to the golden ratio through the dodecahedron, a twelve-faced solid whose geometry involves φ. The framework defines a dimensionless bias proxy, 1 - 1/φ, which it associates with the deviation from linearity. This connection is a modeling choice, not a derivation: the framework chooses to relate the angle to φ, but it does not prove that φ forces the angle.

The framework also makes predictions for water and ammonia. It predicts a water bond angle of about 104.5 degrees by subtracting 5 degrees from the tetrahedral angle, and an ammonia angle of about 107 degrees by subtracting 2.5 degrees. These are definitions with a stated rationale, not proved results. The framework lists explicit falsification criteria: if the cosine of the tetrahedral angle were not -1/3, or if the trend CH₄ > NH₃ > H₂O were violated, the derivation would fail.

What the declaration does not claim is broader than what it does. It does not claim that the formula cos(θ) = -1/(n-1) is a physical law; it is a formula the framework chooses to define. It does not claim that the golden ratio is the cause of the tetrahedral angle; the φ-connection is a stated analogy. And it does not claim that the water and ammonia predictions are derived; they are approximations built from the tetrahedral value.

THEOREM tetrahedral_cosine · IndisputableMonolith/Chemistry/BondAngles.lean
/-- Tetrahedral (n=4) has angle ≈ 109.47° (cos = -1/3). -/
theorem tetrahedral_cosine : optimalBondCosine 4 = -1/3 := by
  simp only [optimalBondCosine]
  norm_num
THEOREM tetra_cos_eq · IndisputableMonolith/Chemistry/BondAngles.lean
/-- 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
THEOREM tetra_angle_bounds · IndisputableMonolith/Chemistry/BondAngles.lean
/-- 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
MODEL optimalBondCosine · IndisputableMonolith/Chemistry/BondAngles.lean
/-- 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 : ℝ)

What this page does not claim

The formula cos(θ) = -1/(n-1) is a derived physical law. The golden ratio causes or forces the tetrahedral angle. The water and ammonia angle predictions are derived from the framework. The framework proves the octahedral angle is 90 degrees.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND