optimalBondCosine
plain-language theorem explainer
The formula for the cosine of the optimal bond angle with n equivalent bonds around a central atom is zero for n at most 1 and negative one over n minus one otherwise. Researchers deriving molecular geometries inside the Recognition Science phi-lattice cite this expression for linear, trigonal, tetrahedral, and octahedral cases. The declaration is a direct conditional definition that downstream results unfold and normalize.
Claim. The optimal cosine of the bond angle for $n$ equivalent bonds is $0$ when $nleq 1$ and $-1/(n-1)$ when $ngeq 2$.
background
The module sets bond angles inside the phi-lattice under CH-014. For n equivalent bonds the optimal angle minimizes electrostatic repulsion while preserving bond strength, producing the cosine formula. The tetrahedral instance with n=4 yields cosine negative one third, or approximately 109.47 degrees, tied to the dodecahedron through phi.
proof idea
The declaration is a definition that directly encodes the formula via a conditional expression: zero for n at most 1, otherwise negative one over n minus one. No lemmas are applied; the body is the explicit arithmetic. Downstream results unfold the definition and normalize the resulting rational number.
why it matters
This definition supplies the common expression for the linear cosine theorem at n=2, the trigonal cosine theorem at n=3, the tetrahedral cosine theorem at n=4, and the octahedral formula cosine at n=6. It realizes the RS mechanism for bond angles from the phi-lattice, linking to the dodecahedral structure and the eight-tick octave. It completes the CH-014 derivation step for angle prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.