FlatInteriorLedger
plain-language theorem explainer
A flat-interior ledger pairs any simplicial ledger with an assignment of flat metrics to its simplices, enforcing Euclidean or Minkowski interiors inside each cell. Researchers modeling Regge calculus or piecewise-flat manifolds cite the structure to guarantee zero curvature within simplices and faces. The declaration is a bare structure definition that directly bundles the base ledger with the per-simplex metric requirement.
Claim. Let $L$ be a simplicial ledger. A flat-interior ledger on $L$ consists of the base $L$ together with a map sending each simplex $σ$ of $L$ to a flat-interior metric $m_σ$ whose signature lies in ${+1,-1}$ and whose Cayley-Menger positivity witness ensures a flat realization in Euclidean or Minkowski space.
background
The module supplies the explicit flat-interior structure required by Regge calculus, where each top-dimensional simplex is isometric to flat space and curvature is supported only on codimension-2 hinges. A FlatInteriorMetric records the signature choice (+1 for Euclidean, -1 for Minkowski) plus a positivity condition on the Cayley-Menger determinant that certifies the edge lengths admit a flat embedding. The module documentation states that any loop confined to the interior of a simplex or crossing only faces returns the identity holonomy.
proof idea
The declaration is a structure definition with an empty proof body. It directly encodes the required property by requiring the metric field to return a FlatInteriorMetric instance for every simplex belonging to the base ledger.
why it matters
The structure is the immediate prerequisite for canonicalEuclideanEnrichment and canonicalMinkowskiEnrichment, which together populate the master InteriorFlatCert that resolves Beltracchi §7. It also supplies the flatness hypothesis used by the interior_jcost_const_consistent theorem to show that J-cost is stationary inside each simplex. In the Recognition framework the construction places curvature exclusively on codimension-2 strata, consistent with the piecewise-flat manifold underlying the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.