DihedralAngleCert
plain-language theorem explainer
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 (
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.