InteriorFlatCert
plain-language theorem explainer
The InteriorFlatCert structure certifies that every 3-simplex admits both a Euclidean flat interior metric and a Minkowski one, that curvature deficits are zero on all non-hinge strata, and that any simplicial ledger admits flat enrichments in both signatures. Regge-calculus and discrete-gravity researchers cite it to guarantee trivial holonomy for interior loops. The declaration is a structure definition whose four fields are witnessed by sibling constructions such as defaultEuclideanInterior and curvature_only_on_hinges.
Claim. Let $L$ be a simplicial ledger and let $s$ be a non-hinge stratum of $L$ (an interior or shared face of a 3-simplex). For every 3-simplex $σ$ there exists a flat interior metric $m$ on $σ$ with signature $+1$ (Euclidean) and one with signature $-1$ (Minkowski). The curvature deficit on $s$ is zero. There exist maps sending any simplicial ledger to a flat-interior ledger in Euclidean signature and in Lorentzian signature.
background
A Simplex3 is the basic volume element: four vertices in $ℝ^3$ with positive volume. A SimplicialLedger is a nonempty collection of such simplices forming a manifold covering. FlatInteriorMetric on a simplex records a signature $±1$ together with a Cayley-Menger positivity witness that the given edge lengths realize flat geometry in the chosen signature. NonHingeStratum comprises codimension-0 interiors and codimension-1 faces; deficitOnNonHinge is defined to be identically zero on these strata. FlatInteriorLedger augments any simplicial ledger by assigning a FlatInteriorMetric to every simplex.
proof idea
This is a structure definition that packages four properties. Each field is an existence or zero-deficit assertion. The concrete witnesses are supplied downstream in interiorFlatCert, which applies defaultEuclideanInterior, defaultMinkowskiInterior, and curvature_only_on_hinges to populate the fields.
why it matters
The certificate directly addresses Beltracchi §7 by making explicit that every simplex interior is flat, so curvature is supported only on codimension-2 hinges. It feeds the downstream construction interiorFlatCert and confirms that the simplicial ledger respects piecewise-flat geometry with trivial holonomy inside simplices. In the Recognition Science framework this localizes curvature exactly where the eight-tick octave and three-dimensional spatial structure require it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.