trigonal_cosine
plain-language theorem explainer
Trigonal planar geometry with three bonds has optimal cosine exactly -1/2 under the J-cost minimization rule. Chemists modeling molecular geometries inside the Recognition Science φ-lattice would cite this entry when tabulating standard bond angles. The proof is a one-line wrapper that unfolds the optimalBondCosine definition and normalizes the arithmetic.
Claim. For three equivalent bonds the optimal bond-angle cosine satisfies $cos(theta_opt) = -1/2$.
background
The module derives bond angles from the φ-lattice by minimizing J-cost for n equivalent bonds around a central atom. The governing formula is cos(θ) = -1/(n-1) for n ≥ 2, producing the table: linear (n=2, cos=-1), trigonal planar (n=3, cos=-1/2), tetrahedral (n=4, cos=-1/3), octahedral (n=6, cos=0). The upstream definition optimalBondCosine encodes this rule directly: if n ≤ 1 then 0 else -1/(n-1 : ℝ).
proof idea
One-line wrapper that applies simp only [optimalBondCosine] followed by norm_num to evaluate the division for n=3.
why it matters
This theorem supplies the trigonal planar row in the bond-angle table of Chemistry.BondAngles. It instantiates the general optimalBondCosine formula for n=3 and thereby supports the RS claim that angles arise from J-cost minimization. The module links the broader set of angles to the φ-lattice via the dodecahedron, though the n=3 case remains purely algebraic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.