Chemistry Bond Angles Linear Cosine

The linear bond angle

A bond angle is the angle formed by two bonds that share a common atom. In a linear molecule, the two bonds point in exactly opposite directions, so the angle between them is 180 degrees. The cosine of 180 degrees is -1. The Recognition Science declaration linear_cosine establishes precisely this fact within its framework: it proves that the optimal cosine for two equivalent bonds is -1, which corresponds to a 180-degree angle.

The framework arrives at this through a general formula for the optimal angle between n equivalent bonds. The formula states that the cosine of the optimal angle equals -1 divided by (n - 1). For two bonds, this gives -1 divided by 1, which is -1. The same formula produces the familiar angles for other common geometries: 120 degrees for three bonds (trigonal planar), 109.47 degrees for four bonds (tetrahedral), and 90 degrees for six bonds (octahedral). The declaration linear_cosine is the machine-checked proof that the formula yields -1 when n equals 2.

In Recognition Science, this result is part of a broader attempt to derive chemical structure from a cost function. The framework models the optimal arrangement of bonds as one that minimizes a certain cost while maintaining bond strength. The tetrahedral angle, for instance, is derived by minimizing this cost for four equivalent bonds. The linear case is the simplest instance of the same principle, and the declaration confirms that the framework's formula reproduces the expected outcome for the two-bond case.

What linear_cosine does not claim is more limited than what it establishes. It does not claim that real molecules with two bonds are always linear; it only states what the framework's formula gives for the ideal case of two equivalent bonds. It does not derive the formula itself from first principles within this declaration; the formula is a definitional choice in the framework. And it does not provide any experimental evidence that real two-bond molecules are linear, which is a separate empirical matter.

/-- Linear geometry (n=2) has angle = 180° (cos = -1). -/
theorem linear_cosine : optimalBondCosine 2 = -1 := by
  simp only [optimalBondCosine]
  norm_num

/-- Optimal cosine of bond angle for n equivalent bonds.
    cos(θ_opt) = -1/(n-1) for n ≥ 2. -/
def optimalBondCosine (n : ℕ) : ℝ :=
  if n ≤ 1 then 0 else -1 / (n - 1 : ℝ)

What this page does not claim

Real molecules with two bonds are always linear. The formula for optimal bond angle is derived from first principles within this declaration. Experimental evidence for linear geometry is provided by this declaration.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/BondAngles.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: