theorem
proved
term proof
tetrahedral_cosine
show as:
view Lean formalization →
formal statement (Lean)
77theorem tetrahedral_cosine : optimalBondCosine 4 = -1/3 := by
proof body
Term-mode proof.
78 simp only [optimalBondCosine]
79 norm_num
80
81/-- Octahedral (n=6) gives cos = -1/5 from formula, but real octahedral uses 90°. -/