totalTheta
plain-language theorem explainer
The definition totalTheta sums the individual dihedral angles contributed by each top simplex sharing a given hinge. Workers on Regge calculus and discrete gravity cite it when writing the deficit or invoking Schläfli's identity to simplify the variation of the action. The body is a one-line wrapper that delegates the summation to the list-sum operation on the dihedral theta components.
Claim. Let $h$ be a simplicial hinge datum consisting of a nonnegative area and a list of dihedral angles $θ_σ$ from the top simplices meeting the hinge. The total dihedral angle at the hinge is defined by $θ_h := ∑_σ θ_σ$.
background
The Schläfli module formalizes the classical identity for piecewise-flat simplicial complexes that reduces the Regge variation to a single term. A SimplicialHingeData record packages the hinge area together with the list of dihedral angles contributed by each top simplex sharing the hinge; the total dihedral angle is the sum of those angles and the deficit is 2π minus the sum. The upstream sumThetas definition maps each dihedral datum to its theta component and sums the resulting list.
proof idea
The definition is a one-line wrapper that applies the sumThetas function from the DihedralAngle module directly to the dihedrals field of the input hinge data.
why it matters
This definition supplies the total angle required by deficit_eq and by schlaefli_kills_dtheta, which in turn feeds LinearizationCoefficients. It forms part of Phase C3 of the program to discharge the Regge deficit linearization hypothesis. The module records Schläfli's identity as a named hypothesis because Mathlib lacks the ambient geometric calculus needed to prove the identity internally; the identity is the step that reduces the Regge equations to the Einstein equations in the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.