tetra_angle_bounds
plain-language theorem explainer
The tetrahedral bond angle satisfies π/2 < arccos(-1/3) < 2π/3. Chemists working in Recognition Science models of molecular geometry cite this bound to place the arccos(-1/3) value strictly inside the 90°–120° interval. The proof splits the conjunction and applies the strict decrease of arccos on [-1,1] twice, once against cos(π/2)=0 and once against the lemma cos(2π/3)=-1/2.
Claim. $π/2 < arccos(-1/3) < 2π/3$
background
The module derives bond angles by minimizing J-cost for n equivalent bonds around a central atom, yielding the rule cos(θ) = -1/(n-1). For tetrahedral geometry (n=4) this fixes cos(θ) = -1/3, so the angle in radians is defined as arccos(-1/3). The local setting is the φ-lattice treatment of CH₄ geometry, where the same angle appears in the dodecahedral embedding and supplies the bias proxy 1-1/φ. The upstream lemma cos(2π/3) = -1/2 supplies the comparison value needed for the upper bound.
proof idea
The tactic proof opens with constructor. The left conjunct rewrites the definition, notes -1/3 < 0, invokes Real.strictAntiOn_arccos on the interval endpoints, and substitutes arccos(0) = π/2. The right conjunct likewise rewrites, notes -1/3 > -1/2, invokes strictAntiOn_arccos, then uses the lemma cos_two_pi_div_three together with arccos_cos to replace arccos(-1/2) by 2π/3.
why it matters
The declaration supplies the numerical interval required by the module’s subsequent CH₄ and water angle predictions. It closes the elementary verification that arccos(-1/3) lies between the linear and trigonal limits inside the Recognition Science bond-angle table. The result sits inside the φ-lattice derivation of tetrahedral geometry and supports the claim that the same angle arises from J-cost minimization on four bonds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.