tetra_bias

formal source

  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