tetra_cos_eq
plain-language theorem explainer
The declaration proves that the cosine of the tetrahedral bond angle equals exactly -1/3. Chemists working within Recognition Science cite this when confirming the geometry that minimizes J-cost for four equivalent bonds around a central atom. The proof is a term-mode reduction that substitutes the angle definition and applies the cosine-arccos identity after numerical bounds checks.
Claim. $cos(θ) = -1/3$, where $θ$ is the tetrahedral bond angle in radians.
background
The module derives bond angles from the φ-lattice by minimizing J-cost for n equivalent bonds, yielding the general relation $cos(θ) = -1/(n-1)$. For tetrahedral geometry with n=4 this specializes to $cos(θ) = -1/3$ and $θ ≈ 109.47°$. The upstream definition supplies the concrete value: tetrahedralAngleRadians is defined as Real.arccos(-1/3). The module table lists the corresponding angles for linear (180°), trigonal planar (120°), and octahedral (90°) cases.
proof idea
The term proof first rewrites tetrahedralAngleRadians to its defining expression arccos(-1/3). It then applies the lemma Real.cos_arccos, discharging the two side conditions that the argument lies in [-1,1] by norm_num.
why it matters
This theorem supplies the explicit cosine value that anchors the tetrahedral entry in the bond-angle table of the Chemistry.BondAngles module. The module documentation ties the angle to J-cost minimization and notes its φ-lattice connection through the dodecahedron. The result therefore closes one concrete prediction step in the RS chemistry layer that begins from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.