theta_le_pi
plain-language theorem explainer
The declaration proves that any dihedral angle θ defined by arccos of a cosine in [-1,1] satisfies θ ≤ π. Researchers formalizing Regge calculus on simplicial complexes cite it to confirm the classical range before handling deficits. The proof is a one-line term application of the standard arccos upper bound lemma to the cosine field.
Claim. Let $d$ be a structure carrying a real number $c$ with $-1 ≤ c ≤ 1$. Define $θ = arccos(c)$. Then $θ ≤ π$.
background
This module sets up dihedral angles at edges of simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis. DihedralAngleData is a structure holding a cosine value in [-1,1] together with the definition θ := arccos(cosine). The module proves the range [0,π] unconditionally, matching classical geometry for tetrahedra and cubes. Upstream, an identical structure appears in Gravity.ReggeCalculus where the regular tetrahedron case gives θ = arccos(1/3).
proof idea
The proof is a one-line term wrapper that applies the library lemma Real.arccos_le_pi directly to the cosine component of the input DihedralAngleData.
why it matters
It supplies the upper bound half of the range fact consumed by dihedralAngleCert, which certifies cube right angles, regular tetrahedron placement in (0,π), and zero deficit on cubic lattices. The result fills the basic range requirement stated in the module doc for Phase C2 before Schläfli identities in Phase C3. It supports the eight-tick octave and D=3 geometry landmarks by ensuring dihedral angles remain in the physically admissible interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.