  60
  61/-- Optimal cosine of bond angle for n equivalent bonds.
  62    cos(θ_opt) = -1/(n-1) for n ≥ 2. -/
  63def optimalBondCosine (n : ℕ) : ℝ :=
  64  if n ≤ 1 then 0 else -1 / (n - 1 : ℝ)
  65
  66/-- Linear geometry (n=2) has angle = 180° (cos = -1). -/
  67theorem linear_cosine : optimalBondCosine 2 = -1 := by
  68  simp only [optimalBondCosine]
  69  norm_num
  70
  71/-- Trigonal planar (n=3) has angle ≈ 120° (cos = -1/2). -/
  72theorem trigonal_cosine : optimalBondCosine 3 = -1/2 := by
  73  simp only [optimalBondCosine]
  74  norm_num
  75
  76/-- Tetrahedral (n=4) has angle ≈ 109.47° (cos = -1/3). -/
  77theorem tetrahedral_cosine : optimalBondCosine 4 = -1/3 := by
  78  simp only [optimalBondCosine]
  79  norm_num
  80
  81/-- Octahedral (n=6) gives cos = -1/5 from formula, but real octahedral uses 90°. -/
  82theorem octahedral_formula_cosine : optimalBondCosine 6 = -1/5 := by
  83  simp only [optimalBondCosine]
  84  norm_num
  85
  86/-! ## Tetrahedral Angle in Degrees -/
  87
  88/-- Tetrahedral angle in radians. -/
  89def tetrahedralAngleRadians : ℝ := Real.arccos (-1/3)
  90
  91/-- Tetrahedral angle in degrees (approximately 109.47°). -/
  92def tetrahedralAngleDegrees : ℝ := tetrahedralAngleRadians * (180 / π)
  93

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.