cos_theta
plain-language theorem explainer
The theorem states that for DihedralAngleData d the cosine of its arccos-defined angle recovers the stored cosine value exactly. Researchers formalizing Regge calculus or simplicial geometry in Recognition Science cite it to certify angle consistency before Schläfli identities. The proof is a one-line wrapper that unfolds the theta definition and invokes the standard cos(arccos x) = x identity on the supplied bounds.
Claim. For any DihedralAngleData $d$ with cosine value $c$ satisfying $-1 ≤ c ≤ 1$, let $θ = arccos(c)$; then $cos(θ) = c$.
background
The module constructs dihedral angles for simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis. DihedralAngleData is the structure carrying a real cosine together with explicit bounds confirming membership in [-1, 1]; its theta field is defined as Real.arccos of that cosine, guaranteeing the angle lies in [0, π]. The same structure appears in Gravity.ReggeCalculus, where it parameterizes the angle between faces sharing an edge of a tetrahedron.
proof idea
The term proof unfolds DihedralAngleData.theta to obtain Real.arccos d.cosine, then applies the library fact Real.cos_arccos directly to the fields cosine_lb and cosine_ub.
why it matters
It supplies the round-trip identity required by the downstream theorem dihedralAngleCert, which certifies the regular-tetrahedron angle arccos(1/3), the cube right angle, and flat-sum conditions. The result closes the minimal honest formalization step in the module doc before Phase C3 Schläfli work and supports the Recognition framework's treatment of angle sums at edges in D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.