waterAnglePrediction
plain-language theorem explainer
WaterAnglePrediction supplies a numerical estimate for the H2O bond angle by subtracting a fixed 5-degree lone-pair correction from the tetrahedral angle. Chemists using Recognition Science would cite it when testing φ-lattice geometry predictions against the observed 104.5° value. The definition is a direct arithmetic adjustment with no additional lemmas or reductions.
Claim. The predicted water bond angle is given by $θ = θ_{tetra} - 5$, where $θ_{tetra} = arccos(-1/3) · (180/π) ≈ 109.47°$ is the angle that minimizes J-cost for four equivalent bonds.
background
The module derives bond angles from the φ-lattice by minimizing J-cost for n equivalent bonds around a central atom. For tetrahedral geometry (n=4) the cosine formula cos(θ) = -1/(n-1) yields cos(θ) = -1/3 and θ ≈ 109.47°. The tetrahedralAngleDegrees definition converts the radian form to degrees via multiplication by 180/π. The module notes that the tetrahedral angle also connects to φ through dodecahedral geometry and that the bias proxy 1 - 1/φ captures deviations from linearity.
proof idea
One-line definition that subtracts the constant 5 from the upstream tetrahedralAngleDegrees value to encode the lone-pair pressure adjustment stated in the doc-comment.
why it matters
The definition extends the tetrahedral derivation in the Bond Angles from φ-Lattice section to a concrete water-molecule prediction. It illustrates how RS geometry (cos(θ) = -1/3) is adjusted for lone-pair effects while remaining inside the φ-lattice framework. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.