DihedralAngleCert
DihedralAngleCert bundles the geometric facts needed to certify flat cubic lattices inside the dihedral-angle API: the cube dihedral equals π/2, the regular tetrahedron dihedral lies in (0, π), four cube dihedrals sum to 2π with zero deficit, and every DihedralAngleData yields a theta in [0, π] whose cosine recovers the input. Researchers working on Regge-calculus linearization or simplicial discrete curvature would cite this certificate when discharging flat-space identities. The structure is assembled directly from prior evaluations of cube (
claimA certificate asserting that the cube dihedral angle satisfies $θ = π/2$, the regular tetrahedron dihedral satisfies $0 < θ < π$, the flat-sum condition holds for the list of four cube dihedrals, the deficit of that list vanishes, every dihedral-angle datum $d$ satisfies $0 ≤ θ(d) ≤ π$, and $cos θ(d) = d.cosine$.
background
The module defines dihedral angles at edges of simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis. DihedralAngleData is the structure carrying a cosine in [-1, 1] with theta defined as arccos of that cosine. FlatSumCondition on a list of such data asserts that the sum of thetas equals 2π; deficit is then 2π minus that sum. Cube dihedral is the datum with cosine 0; regular tetrahedron dihedral is the datum with cosine 1/3. These rest on the general range lemmas theta_nonneg and theta_le_pi together with the cosine recovery lemma.
proof idea
The structure is a definition that directly references the evaluated cube_dihedral and regular_tet_dihedral data, the FlatSumCondition instance cubic_lattice_flatSum, the zero-deficit lemma cubic_lattice_deficit_zero, and the general range and cosine lemmas for any DihedralAngleData.
why it matters in Recognition Science
It supplies the flat cubic hinge identity (deficit zero) that lifts the baseline already present in ReggeCalculus.cubic_lattice_flat to the DihedralAngle API. The structure is consumed by the theorem dihedralAngleCert that assembles the full certificate. This closes the elementary flat-space case required before Schläfli's identity (Phase C3) and the final simplicial discharge (Phase C5). It anchors the D = 3 discrete-curvature setting of the Recognition framework.
scope and limits
- Does not derive the cosine formula from Cayley-Menger minors.
- Does not treat dihedral angles of irregular tetrahedra or higher simplices.
- Does not prove Schläfli's identity or the full Regge linearization.
- Does not address non-flat hinges or curvature defects beyond the cubic lattice case.
formal statement (Lean)
160structure DihedralAngleCert where
161 cube_is_right_angle : cube_dihedral.theta = Real.pi / 2
162 regular_tet_in_range :
163 0 < regular_tet_dihedral.theta ∧ regular_tet_dihedral.theta < Real.pi
164 cubic_flat_sum :
165 FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral]
166 cubic_deficit_zero :
167 deficit [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] = 0
168 theta_in_range : ∀ d : DihedralAngleData, 0 ≤ d.theta ∧ d.theta ≤ Real.pi
169 cos_theta_eq : ∀ d : DihedralAngleData, Real.cos d.theta = d.cosine
170