dihedralAngleCert
Researchers in discrete differential geometry and Regge calculus cite the dihedral angle certificate when verifying flat-space baselines on cubic lattices and regular tetrahedra. It packages the exact right-angle property of the cube, the open-interval range of the regular tetrahedron angle, the flat sum of four right angles equaling 2π, and the vanishing deficit together with the general range and cosine recovery for arbitrary dihedral data. The proof is a direct term-mode construction that instantiates each field of the certificate structure.
claimThere exists a certificate such that the cube dihedral angle equals exactly $π/2$, the regular tetrahedron dihedral angle $θ$ satisfies $0 < θ < π$, four cube angles satisfy the flat sum condition, the associated deficit vanishes, every dihedral angle data has $θ$ in $[0, π]$, and $cos θ$ recovers the input cosine value for any such data.
background
This module defines dihedral angles at edges of simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis. A DihedralAngleData structure carries a cosine value bounded in [-1,1] with theta defined as arccos of that value. The certificate structure collects six properties: the cube angle is right, the regular tetrahedron angle lies in the open interval (0,π), four cube angles sum flatly to 2π, the deficit for that sum is zero, every dihedral angle lies in [0,π], and cosine recovers the input value. Upstream lemmas establish cos θ equals the stored cosine by the arccos identity, the cube angle equals π/2 by arccos zero, four cube angles sum to 2π by direct addition, and the regular tetrahedron angle arccos(1/3) lies strictly between 0 and π.
proof idea
The proof is a term-mode instantiation of the DihedralAngleCert structure. It assigns cube_is_right_angle from the cube dihedral theta lemma, regular_tet_in_range from the open-interval lemma on the regular tetrahedron, cubic_flat_sum from the four-cube flat sum theorem, cubic_deficit_zero from the zero-deficit theorem on the flat sum, theta_in_range from a lambda pairing the nonnegativity and upper-bound lemmas, and cos_theta_eq from the general cosine recovery theorem.
why it matters in Recognition Science
The certificate closes Phase C2 by confirming the classical flat cubic lattice identity (four right angles sum to 2π with zero deficit) and the range properties required for curvature linearization. It directly enables the Schläfli identity in Phase C3 and the final simplicial discharge in Phase C5. It supplies the geometric baseline for the Regge deficit on simplicial complexes without introducing axioms or hidden hypotheses.
scope and limits
- Does not compute dihedral angles for irregular or non-regular tetrahedra.
- Does not derive explicit Cayley-Menger minors for arbitrary edge lengths.
- Does not prove the full Regge deficit linearization hypothesis.
- Does not address curved or non-Euclidean background geometries.
- Does not extend the flat sum condition beyond the cubic lattice case.
formal statement (Lean)
171theorem dihedralAngleCert : DihedralAngleCert where
172 cube_is_right_angle := cube_dihedral_theta
proof body
Term-mode proof.
173 regular_tet_in_range := regular_tet_dihedral_in_open_interval
174 cubic_flat_sum := cubic_lattice_flatSum
175 cubic_deficit_zero := cubic_lattice_deficit_zero
176 theta_in_range := fun d => ⟨theta_nonneg d, theta_le_pi d⟩
177 cos_theta_eq := cos_theta
178
179end
180
181end DihedralAngle
182end Geometry
183end IndisputableMonolith