NonHingeStratum
plain-language theorem explainer
NonHingeStratum classifies the codimension-0 interiors and codimension-1 faces of a simplicial ledger that carry no curvature under the flat-interior axiom. Regge-calculus and piecewise-flat manifold researchers cite it to localize all deficits to codimension-2 hinges. The declaration is a direct inductive definition with two constructors, one for each stratum type.
Claim. An inductive type over a simplicial ledger $L$ whose inhabitants are either the interior of a 3-simplex $σ$ or a 2-face shared by two 3-simplices $σ_1,σ_2$; both strata are assigned zero curvature deficit by the flat-interior axiom.
background
The module formalizes the interior-flat property required by Regge calculus: each 3-simplex is isometric to a flat Euclidean or Minkowski tetrahedron whose edge lengths determine the metric via the Cayley-Menger determinant. A Simplex3 is a structure carrying four vertices in $ℝ^3$ together with a positive volume. A SimplicialLedger is a nonempty set of such simplices that cover a manifold. The DihedralAngle.deficit function computes $2π$ minus the sum of dihedral angles at a hinge; the same function is set to zero on non-hinge strata. Upstream results supply the edge-length map from the ledger and the collision-free program that guarantees consistent metrics.
proof idea
Direct inductive definition. The two constructors interior and face enumerate the allowed strata; no further proof obligations are discharged because the declaration itself encodes the flat-interior axiom.
why it matters
NonHingeStratum supplies the domain for deficitOnNonHinge and curvature_only_on_hinges, which together prove that the Regge curvature sum is supported only on codimension-2 hinges. It is the key datum inside the master certificate InteriorFlatCert that discharges Beltracchi §7 by exhibiting flat Euclidean and Minkowski interiors for every simplex. The construction directly implements the codimension-2 curvature concentration stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.