defaultEuclideanInterior
plain-language theorem explainer
Every 3-simplex of positive volume carries a default Euclidean flat-interior metric by direct construction. Regge calculus and discrete gravity workers cite this to guarantee that interior paths incur no holonomy. The definition assembles the metric record from the simplex volume positivity witness.
Claim. For any 3-simplex $σ$ with volume $>0$, the default Euclidean interior metric is the structure with signature $+1$, Cayley-Menger positivity witnessed by $vol(σ)>0$, and trivial flat interior.
background
A Simplex3 is a tetrahedron with four vertices in $ℝ^3$ and a positive volume field. FlatInteriorMetric on such a simplex records a signature in {+1, -1}, a proof that the signature is ±1, a Cayley-Menger positivity proposition, and a flat-interior flag. The module addresses Beltracchi §7 by making explicit that each top-dimensional simplex in a Regge triangulation carries a flat metric whose curvature is confined to codimension-2 hinges.
proof idea
Direct construction of the FlatInteriorMetric record: signature set to 1, signature condition discharged by reflexivity, Cayley-Menger positivity taken from the simplex volume field, and flat interior set to True.
why it matters
This definition supplies the Euclidean case for canonicalEuclideanEnrichment, which in turn populates interiorFlatCert. It realizes the Regge axiom that curvature is supported only on codimension-2 hinges, closing the interior-flat part of the simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.