IndisputableMonolith.Chemistry.BondAngles

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Compat
   4
   5open Real Complex
   6open scoped BigOperators Matrix
   7
   8/-!
   9# Bond Angles from φ-Lattice (CH-014)
  10
  11## Tetrahedral Angle Derivation
  12
  13The tetrahedral bond angle θ = 109.47° = arccos(-1/3) arises from
  14minimizing J-cost for 4 equivalent bonds around a central atom.
  15
  16**RS Mechanism**:
  17For n equivalent bonds, the optimal angle minimizes electrostatic repulsion
  18while maintaining bond strength. The formula is:
  19  cos(θ) = -1/(n-1)
  20
  21For tetrahedral geometry (n=4):
  22  cos(θ) = -1/3
  23  θ = arccos(-1/3) ≈ 109.47°
  24
  25**φ-Connection**:
  26The tetrahedral angle relates to φ through the dodecahedron:
  27- Dodecahedron edge-center angle involves φ
  28- Regular tetrahedron inscribed in cube has this angle
  29- The bias proxy `1 - 1/φ` captures the deviation from linearity
  30
  31## Bond Angle Predictions
  32
  33| Geometry | n bonds | cos(θ) | θ |
  34|----------|---------|--------|---|
  35| Linear | 2 | -1 | 180° |
  36| Trigonal planar | 3 | -1/2 | 120° |
  37| Tetrahedral | 4 | -1/3 | 109.47° |
  38| Octahedral | 6 | 0 | 90° |
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Chemistry
  43
  44noncomputable section
  45
  46/-- Dimensionless bias proxy for tetrahedral preference. -/
  47def tetra_bias : ℝ := 1 - (1 / Constants.phi)
  48
  49/-- The bias proxy is strictly positive (since φ>1 ⇒ 1/φ<1). -/
  50theorem angle_bias : 0 < tetra_bias := by
  51  dsimp [tetra_bias]
  52  have hφ : 1 < Constants.phi := Constants.one_lt_phi
  53  have hφpos : 0 < Constants.phi := lt_trans (by norm_num) hφ
  54  have h_inv_lt : (1 / Constants.phi) < 1 := by
  55    rw [div_lt_one hφpos]
  56    exact hφ
  57  exact sub_pos.mpr h_inv_lt
  58
  59/-! ## Optimal Bond Angle for n Equivalent Bonds -/
  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
  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
  98  · norm_num
  99  · norm_num
 100
 101/-- cos(2π/3) = -1/2 -/
 102private lemma cos_two_pi_div_three : Real.cos (2 * π / 3) = -1/2 := by
 103  -- 2π/3 = π - π/3, and cos(π - x) = -cos(x)
 104  have h : (2 : ℝ) * π / 3 = π - π / 3 := by ring
 105  rw [h, Real.cos_pi_sub, Real.cos_pi_div_three]
 106  norm_num
 107
 108/-- The tetrahedral angle is between 90° and 120° (in radians).
 109    90° = π/2 ≈ 1.571, 120° = 2π/3 ≈ 2.094
 110    arccos(-1/3) ≈ 1.911 -/
 111theorem tetra_angle_bounds :
 112    π/2 < tetrahedralAngleRadians ∧ tetrahedralAngleRadians < 2*π/3 := by
 113  constructor
 114  · -- θ > 90° because cos(θ) = -1/3 < 0 = cos(90°)
 115    rw [tetrahedralAngleRadians]
 116    have h_neg : (-1/3 : ℝ) < 0 := by norm_num
 117    -- arccos is strictly decreasing, so arccos(-1/3) > arccos(0) = π/2
 118    have h_zero_in : (0 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]
 119    have h_third_in : (-1/3 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]; norm_num
 120    have h_mono := Real.strictAntiOn_arccos h_third_in h_zero_in h_neg
 121    rwa [Real.arccos_zero] at h_mono
 122  · -- θ < 120° because cos(θ) = -1/3 > -1/2 = cos(120°)
 123    rw [tetrahedralAngleRadians]
 124    have h_neg_third_gt : (-1/3 : ℝ) > -1/2 := by norm_num
 125    have h_half_in : (-1/2 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]; norm_num
 126    have h_third_in : (-1/3 : ℝ) ∈ Set.Icc (-1 : ℝ) 1 := by simp [Set.mem_Icc]; norm_num
 127    have h_mono := Real.strictAntiOn_arccos h_half_in h_third_in h_neg_third_gt
 128    -- cos(2π/3) = -1/2, so arccos(-1/2) = 2π/3
 129    have h_in_range : 0 ≤ 2 * π / 3 ∧ 2 * π / 3 ≤ π := by
 130      constructor
 131      · positivity
 132      · have hp := Real.pi_pos
 133        linarith
 134    have h_arccos : Real.arccos (-1/2) = 2 * π / 3 := by
 135      rw [← cos_two_pi_div_three]
 136      exact Real.arccos_cos h_in_range.1 h_in_range.2
 137    rwa [h_arccos] at h_mono
 138
 139/-! ## CH₄ and Water Angle Predictions -/
 140
 141/-- Methane (CH₄) bond angle = tetrahedral angle. -/
 142def methaneAngle : ℝ := tetrahedralAngleDegrees
 143
 144/-- Water (H₂O) bond angle is slightly less than tetrahedral due to lone pairs.
 145    Observed: 104.5°. RS predicts deviation from lone pair pressure. -/
 146def waterAnglePrediction : ℝ := tetrahedralAngleDegrees - 5  -- Approximate LP correction
 147
 148/-- Ammonia (NH₃) bond angle is between water and tetrahedral.
 149    Observed: 107°. -/
 150def ammoniaAnglePrediction : ℝ := tetrahedralAngleDegrees - 2.5  -- One LP
 151
 152/-! ## Falsification Criteria
 153
 154The tetrahedral angle derivation is falsifiable:
 155
 1561. **Cosine value**: If cos(tetrahedral angle) ≠ -1/3 for sp³ carbon
 157
 1582. **Trend violation**: If bond angle doesn't decrease with lone pairs:
 159   CH₄ (109.5°) > NH₃ (107°) > H₂O (104.5°)
 160
 1613. **Formula violation**: If cos(θ) ≠ -1/(n-1) for other geometries
 162-/
 163
 164end
 165
 166end Chemistry
 167end IndisputableMonolith
 168