theta_le_pi
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the matching lower bound θ ≥ 0.
- Does not evaluate explicit angles for any concrete polyhedron.
- Does not address angle sums around an edge or flat-sum conditions.
- Does not invoke the Cayley-Menger determinant beyond the supplied cosine bound.
formal statement (Lean)
68theorem theta_le_pi (d : DihedralAngleData) : d.theta ≤ Real.pi :=
proof body
Term-mode proof.
69 Real.arccos_le_pi d.cosine
70
71/-- `cos θ = cosine` by construction. -/