canonicalEuclideanEnrichment
plain-language theorem explainer
The definition equips any simplicial ledger with a flat Euclidean interior metric on every simplex. Researchers formalizing Regge calculus or piecewise-flat manifolds in Recognition Science cite it to instantiate the interior-flat structure required by the ledger. It is realized by a direct one-line construction that assigns the default Euclidean interior to each simplex.
Claim. For any simplicial ledger $L$, the canonical Euclidean enrichment is the flat-interior ledger whose base is $L$ and whose metric assigns the default Euclidean interior to every simplex of $L$.
background
The Interior-Flat Simplices module addresses Beltracchi §7 by making explicit that each simplex in a Regge-calculus manifold carries a flat Euclidean or Minkowski interior. A flat-interior ledger is a simplicial ledger in which every simplex is equipped with a flat-interior metric structure, formalizing the requirement that ledger cells are filled with flat space. Curvature is confined to codimension-two hinges while interiors and faces remain flat, so interior loops carry trivial holonomy.
proof idea
This is a one-line wrapper that applies defaultEuclideanInterior to populate the metric field of the FlatInteriorLedger structure.
why it matters
It supplies the euclidean_enrichment field inside interiorFlatCert, which certifies Euclidean and Minkowski enrichments together with curvature restricted to codimension-two hinges. The definition therefore closes the explicit treatment of interior-flat simplices in the Recognition Science simplicial ledger, consistent with the framework's piecewise-flat manifold axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.