deficit_pos_of_angle_deficit
plain-language theorem explainer
The theorem shows that the deficit angle at a hinge is strictly positive when the sum of its dihedral angles falls below 2π, which encodes positive curvature in the simplicial lattice. Discrete gravity researchers on the RS lattice cite this when signing curvature contributions to the Regge action. The proof is a one-line wrapper that unfolds the deficit definition and invokes linear arithmetic on the supplied inequality.
Claim. Let $h$ be a hinge datum consisting of a positive area and a list of dihedral angles. If the sum of those angles is strictly less than $2π$, then the deficit angle $2π$ minus the sum is positive.
background
The module formalizes Regge calculus on the RS lattice, replacing linearized deficit assumptions with exact piecewise-flat geometry. Curvature concentrates on codimension-2 hinges; the Regge action sums area times deficit angle over all hinges. HingeData is the structure carrying a positive real area together with the list of dihedral angles meeting at that hinge. The deficit angle itself is defined upstream as $2π$ minus the sum of those dihedral angles.
proof idea
The proof is a one-line wrapper that unfolds the definition of deficit_angle and applies linarith to the hypothesis that the angle sum is less than $2π$.
why it matters
This result supplies the deficit_positive field inside regge_calculus_cert, which certifies the full Regge machinery for the discrete gravity programme. It directly supports the sign of curvature terms in the Regge action when the lattice exhibits positive curvature, consistent with the eight-tick octave and three-dimensional spatial structure of the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.