interiorFlatCert
plain-language theorem explainer
interiorFlatCert supplies the master certificate asserting that every 3-simplex in any simplicial ledger carries both Euclidean and Minkowski flat interiors while confining all curvature to codimension-two hinges. Regge-calculus modelers and discrete-gravity researchers cite it to close the interior-flat axiom required by Beltracchi §7. The definition assembles the certificate directly from the default interior metrics and the zero-deficit theorem on non-hinge strata.
Claim. For any simplicial ledger $L$, every 3-simplex admits a flat Euclidean interior metric of signature $+1$, a flat Minkowski interior metric of signature $-1$, the curvature deficit vanishes on every non-hinge stratum, and $L$ admits canonical Euclidean and Minkowski enrichments to a flat-interior ledger.
background
SimplicialLedger collects a nonempty set of 3-simplices that form a manifold covering (scaffold). InteriorFlatCert is the master structure that records four properties: existence of flat Euclidean interiors for every simplex, existence of flat Minkowski interiors, zero deficit on non-hinge strata, and canonical enrichments of any ledger to a flat-interior ledger. The module addresses Beltracchi §7 by making explicit that piecewise-flat manifolds carry flat interiors inside simplices and across faces, with curvature concentrated on codimension-2 hinges. Upstream, defaultEuclideanInterior and defaultMinkowskiInterior construct the metrics from volume positivity via Cayley-Menger, while curvature_only_on_hinges proves the deficit vanishes by reflexivity. canonicalEuclideanEnrichment and canonicalMinkowskiEnrichment wrap any ledger with these defaults.
proof idea
Record construction that populates the four fields of InteriorFlatCert: euclidean_exists applies defaultEuclideanInterior to any simplex, minkowski_exists applies defaultMinkowskiInterior, curvature_codim_two invokes curvature_only_on_hinges, and the two enrichment fields call canonicalEuclideanEnrichment and canonicalMinkowskiEnrichment respectively.
why it matters
This definition closes the interior-flat axiom in the simplicial ledger foundation, directly answering Beltracchi §7 that Regge calculus requires flat interiors with curvature only on hinges. It supplies the concrete certificate that downstream developments in discrete gravity and the Recognition Science simplicial model can invoke without further proof. The construction relies on the ledger structure and zero-deficit theorem; no open question remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.