cos_two_pi_div_three
plain-language theorem explainer
The lemma establishes that cosine of 2π/3 equals negative one half. Chemists deriving trigonal planar bond angles from J-cost minimization for three equivalent bonds would cite this identity to confirm the 120 degree case. The proof rewrites the argument as π minus π/3 via ring, applies the cosine subtraction identity, substitutes the known cosine of π/3, and normalizes.
Claim. $cos(2π/3) = -1/2$
background
The Bond Angles from φ-Lattice module derives optimal angles by minimizing J-cost for n equivalent bonds around a central atom, yielding the general relation cos(θ) = -1/(n-1). J-cost here quantifies the balance between electrostatic repulsion and bond strength in the Recognition Science setting. For n=3 (trigonal planar) this produces cos(θ) = -1/2 at 120 degrees, while n=4 produces the tetrahedral arccos(-1/3).
proof idea
The tactic proof first asserts (2 * π / 3) = π - (π / 3) by ring. It rewrites cosine via the subtraction formula cos(π - x) = -cos(x), substitutes the library fact cos(π/3) = 1/2, and applies norm_num to reach -1/2.
why it matters
This lemma supplies the boundary value used by tetra_angle_bounds to bound the tetrahedral angle between π/2 and 2π/3. It completes the trigonal planar row in the module's bond-angle table, anchoring the n=3 case of the J-cost minimization that produces the tetrahedral geometry for n=4. The result sits inside the φ-lattice derivation linking bond angles to the dodecahedron and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.