cos_theta
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive cosine values from explicit Cayley-Menger minors.
- Does not treat curved or non-Euclidean simplices.
- Does not supply numerical approximations or bounds beyond the exact identity.
- Does not address angle sums or deficits directly.
formal statement (Lean)
72theorem cos_theta (d : DihedralAngleData) : Real.cos d.theta = d.cosine := by
proof body
Term-mode proof.
73 unfold DihedralAngleData.theta
74 exact Real.cos_arccos d.cosine_lb d.cosine_ub
75
76/-! ## §2. Canonical values -/
77
78/-- A regular tetrahedron's dihedral angle has cosine `1/3`. -/