curvature_only_on_hinges
plain-language theorem explainer
In a simplicial ledger, the curvature deficit vanishes on every non-hinge stratum, whether a 3-simplex interior or a shared 2-face. Regge-calculus and piecewise-flat manifold modelers cite the result to localize all curvature to codimension-two hinges. The proof is immediate by reflexivity on the deficit definition for such strata.
Claim. Let $L$ be a simplicial ledger. For any non-hinge stratum $s$ of $L$ (a 3-simplex interior or shared 2-face), the associated deficit equals zero.
background
A simplicial ledger is a collection of 3-simplices forming a manifold covering. Non-hinge strata are the codimension-0 interiors and codimension-1 faces; by the flat-interior axiom these carry no curvature. The module formalizes Philip Beltracchi's §7 requirement that each simplex is filled with flat Euclidean or Minkowski space, so that curvature is concentrated exclusively on codimension-2 hinges (edges in 3D). Upstream, the SimplicialLedger structure supplies the underlying set of simplices and the non-emptiness condition.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of the deficit on non-hinge strata.
why it matters
The theorem is invoked inside interiorFlatCert to certify that curvature support is codimension-two, completing the flat-interior ledger construction. It directly implements the Regge-calculus axiom quoted in the module documentation: curvature is concentrated on codimension-2 subsimplices while codimension-0 and codimension-1 cells carry zero deficit. The result closes the explicit gap between the earlier simplicial ledger and the piecewise-flat manifold demanded by Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.