DihedralAngleData
plain-language theorem explainer
DihedralAngleData packages a real cosine value with the predicate that it lies in the closed interval from -1 to 1. Workers on discrete gravity and Regge calculus cite the structure when they need a certified parameter for the angle between faces of a tetrahedron in a simplicial complex. The declaration is a direct structure definition with no separate proof obligations.
Claim. A dihedral angle datum consists of a real number $c$ satisfying $-1 ≤ c ≤ 1$.
background
The module formalizes exact Regge calculus on the RS lattice, replacing linearized deficit-angle assumptions with the full machinery of piecewise-flat simplicial complexes. Curvature concentrates on codimension-2 hinges, and the Regge action is the sum over hinges of area times deficit angle. Edge lengths are set by the J-cost defect field on the Z^3 × Z lattice. The upstream DihedralAngleData from the geometry layer supplies the basic cosine datum with separate lower and upper bound fields; the present structure bundles them into a single predicate.
proof idea
The declaration is a structure definition with an empty proof body. It directly introduces the cosine field of type ℝ together with the bundled bound predicate -1 ≤ cosine ∧ cosine ≤ 1.
why it matters
The structure supplies the certified cosine input required by downstream definitions and theorems that compute the actual dihedral angle via arccos, construct the right-angle cube case with cosine 0, form deficit angles as 2π minus the sum of dihedrals, and verify flat sums. It therefore supports the Regge action non-negativity and Gauss-Bonnet identities that close the discrete gravity programme, linking directly to the T7 eight-tick octave and D = 3 spatial dimensions of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.