canonicalMinkowskiEnrichment
plain-language theorem explainer
The canonical Minkowski enrichment assigns the default Minkowski interior metric to every simplex in a simplicial ledger. Researchers modeling Lorentzian piecewise-flat manifolds in Recognition Science cite this when enforcing flat interiors per Regge calculus. The definition proceeds by direct structural assignment of the ledger base and the default interior metric function.
Claim. For any simplicial ledger $L$, the canonical Minkowski enrichment is the flat interior ledger whose base is $L$ and whose metric assigns the default Minkowski interior to each simplex.
background
The Interior-Flat Simplices module addresses Beltracchi §7 by making explicit that each simplex carries a flat interior metric, with curvature concentrated exclusively on codimension-2 hinges. A flat interior ledger is a simplicial ledger equipped with a flat-interior metric for every simplex. The simplicial ledger is a nonempty collection of 3-simplices forming a manifold covering, as defined upstream.
proof idea
This is a one-line wrapper that constructs the flat interior ledger by setting its base to the input simplicial ledger and its metric to the function returning the default Minkowski interior on each simplex.
why it matters
It provides the Minkowski enrichment required by the interior flat certificate, which certifies the existence of both Euclidean and Minkowski enrichments together with curvature support restricted to codimension two. The definition fills the explicit flat-interior structure for the simplicial ledger, consistent with the three spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.