defaultMinkowskiInterior
plain-language theorem explainer
This definition supplies the standard Lorentzian interior metric for any 3-simplex in the simplicial ledger. Workers extending Regge calculus to Recognition Science cite it when assigning flat Minkowski structure to tetrahedra in 3+1 embeddings. It is realized as a direct record construction that hard-codes signature -1 and derives positivity from the simplex volume.
Claim. For a 3-simplex $σ$, the default Minkowski interior metric is the structure with signature $-1$, satisfying the signature condition, with Cayley-Menger positivity witnessed by $σ.volume > 0$, and flat interior true.
background
A Simplex3 is a tetrahedron whose four vertices lie in $ℝ^3$ and whose volume is strictly positive. The FlatInteriorMetric structure records a signature choice (+1 for Euclidean, -1 for Minkowski), a positivity witness drawn from the Cayley-Menger determinant on the edge lengths, and the assertion that the interior carries trivial holonomy. This module makes the Regge-calculus principle explicit: curvature is confined to codimension-2 hinges, so any loop that stays inside a single simplex or crosses only faces returns the identity isometry.
proof idea
Direct record construction. Signature is set to -1; the signature condition is discharged by right injection of reflexivity; CM_positive is taken directly from the volume positivity hypothesis on $σ$; flat_interior is set to True.
why it matters
The definition supplies the Minkowski case required by interiorFlatCert and is applied inside canonicalMinkowskiEnrichment to equip every simplicial ledger with default Lorentzian interiors. It thereby closes the Regge axiom that interior holonomy is trivial, consistent with curvature supported only on hinges. In the Recognition framework this underwrites the piecewise-flat geometry compatible with D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.