Hinge
plain-language theorem explainer
A curvature-bearing hinge in a simplicial ledger is a codimension-2 substructure equipped with a real deficit angle, localizing curvature while interiors remain flat. Researchers in discrete gravity or Regge calculus discretizations cite this to enforce curvature support only on edges in 3D. The entry is a bare structure definition with one real field and no computational content.
Claim. For a collection of 3-simplices forming a manifold covering, a curvature-bearing hinge is a codimension-2 substructure equipped with a real-valued deficit angle.
background
The module formalizes the interior-flat axiom to address Beltracchi §7 in Regge calculus: each 3-simplex carries a flat Euclidean or Minkowski metric, and curvature concentrates exclusively on codimension-2 subsimplices. Upstream, the SimplicialLedger structure is defined as a nonempty set of 3-simplices with a manifold-covering property. Hinges are the edges in 3D that receive deficit angles, while codimension-0 interiors and codimension-1 faces carry zero curvature by the flat-interior axiom.
proof idea
This is a structure definition that directly introduces the hinge type parameterized by a simplicial ledger and supplies a single real field for the deficit. No lemmas, tactics, or reductions are applied; the declaration records the object for subsequent use in deficit functionals.
why it matters
The definition supplies the hinge type used by the cubic deficit functional and by conformal edge length results at vanishing vacuum. It implements the Regge principle that curvature lives only on codimension-2 hinges, consistent with the interior-flat property and the three-dimensional setting. This supplies the explicit codimension-2 support required by the Recognition Science simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.