linear_cosine
plain-language theorem explainer
The theorem proves that the optimal bond cosine for two equivalent bonds equals -1, matching linear geometry at 180 degrees. Chemists working with Recognition Science bond-angle tables cite this when applying the J-cost minimization formula across geometries. The proof is a one-line wrapper that unfolds the optimalBondCosine definition and evaluates the resulting arithmetic expression.
Claim. For two equivalent bonds the optimal bond-angle cosine satisfies $cos θ = -1$.
background
The module derives bond angles from the φ-lattice by minimizing J-cost for n equivalent bonds around a central atom. The upstream definition states that optimalBondCosine n equals -1/(n-1) for n ≥ 2, which directly supplies the cosine of the optimal angle θ. The module table lists the linear case (n=2) as the first row with cos θ = -1 at 180°.
proof idea
The proof is a one-line wrapper that applies simp only on optimalBondCosine to unfold the definition, then uses norm_num to compute -1/(2-1) = -1.
why it matters
This result supplies the linear entry in the bond-angle predictions table of the φ-lattice chemistry module (CH-014). It anchors the general formula cos(θ) = -1/(n-1) that generates the trigonal, tetrahedral, and octahedral rows. No downstream uses are recorded and the claim is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.