deficit_neg_of_angle_excess
plain-language theorem explainer
When the sum of dihedral angles around a hinge exceeds 2π the deficit angle is negative, corresponding to negative curvature on the discrete lattice. This lemma is cited inside the Regge calculus certification that validates the full nonlinear action for Recognition Science gravity. The proof is a direct one-line wrapper that unfolds the deficit definition and applies linear arithmetic.
Claim. Let $h$ be a hinge with area $A>0$ and list of dihedral angles whose sum exceeds $2π$. Then the deficit angle satisfies $δ(h)<0$.
background
Regge calculus replaces smooth spacetime by a piecewise-flat simplicial complex in which curvature is concentrated on codimension-2 hinges. The HingeData structure records the hinge area together with the list of dihedral angles contributed by all simplices meeting at that hinge; the deficit angle is defined as $2π$ minus the sum of those dihedral angles. Positive deficit signals positive curvature and negative deficit signals negative curvature, exactly as required for the discrete Einstein-Hilbert action $S=∑A_hδ_h$.
proof idea
The proof is a one-line wrapper: it unfolds the definition of deficit_angle and invokes linear arithmetic on the resulting inequality.
why it matters
The lemma supplies the negative-deficit case required by regge_calculus_cert, which assembles flat vanishing, cubic-lattice flatness, and both curvature signs to certify the Regge framework on the RS lattice. It thereby closes the discrete-gravity side of the Recognition Science programme that replaces the linearized deficit ansatz with exact Regge machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.