`linear_cosine`

proved

show as: view math explainer →

module: IndisputableMonolith.Chemistry.BondAngles
domain: Chemistry
line: 67 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Chemistry.BondAngles on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

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

papers checked against this theorem

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