sumThetas
Defines the total dihedral angle around a hinge by summing the arccos-derived angles from a list of dihedral data entries. Regge calculus and simplicial geometry formalizations cite this to compute curvature deficits at edges. The definition composes a list map onto the angle function with a real summation.
claimFor a finite list $ds$ of dihedral angle data, each equipped with a cosine $c_d$ in $[-1,1]$, the summed angle is $s = sum_{d in ds} arccos(c_d)$.
background
The module develops dihedral angles at edges of tetrahedra from Cayley-Menger data as Phase C2 of the program to formalize the Regge deficit linearization on simplicial complexes. Each dihedral data entry stores a cosine value bounded in $[-1,1]$ and defines its angle via the inverse cosine, which lies in $[0,pi]$. The present definition aggregates these angles over any list of such entries, reproducing the classical sum of face angles around an edge. It reuses the dihedral data structure introduced in the Regge calculus module, where the angle is the dihedral between two faces sharing the edge.
proof idea
One-line wrapper that maps each dihedral data entry to its arccos angle and sums the resulting real values.
why it matters in Recognition Science
The summation enters the deficit computation and the flat-sum condition that marks zero curvature. Downstream theorems apply it to confirm that four right angles from a cubic lattice sum to $2pi$ and to define the total angle in the Schläfli identity for hinges. In the broader framework it supplies the angle aggregate required for discrete curvature on three-dimensional simplicial complexes, advancing the discharge of the Regge hypothesis without introducing new axioms.
scope and limits
- Does not assert equality of the sum to $2pi$.
- Does not impose geometric constraints on the underlying simplices.
- Does not compute the cosine values from edge lengths.
- Does not address cases with fewer or more than the expected number of dihedrals at a hinge.
formal statement (Lean)
126def sumThetas (ds : List DihedralAngleData) : ℝ :=
proof body
Definition body.
127 (ds.map DihedralAngleData.theta).sum
128
129/-- The flat-sum condition: the total dihedral angle at a hinge equals `2π`. -/