FlatInteriorMetric
plain-language theorem explainer
FlatInteriorMetric records a signature choice together with Cayley-Menger positivity and the flat-interior Regge axiom for a given 3-simplex. Discrete gravity researchers cite the structure when formalizing piecewise-flat manifolds in which curvature is confined to hinges. The definition is introduced directly as a record type with no computational content or proof obligations.
Claim. A flat interior metric on a 3-simplex $σ$ consists of an integer signature $s$ with $s=1$ or $s=-1$, a proposition witnessing that the edge lengths admit a flat realization via the Cayley-Menger determinant, and a proposition asserting that the interior is flat with trivial holonomy on any interior loop.
background
The module formalizes the requirement that each simplex in a Regge triangulation carries a flat interior metric. This means the 3-simplex is isometric to the standard simplex in either Euclidean space or Minkowski space, determined solely by its six edge lengths. Curvature arises only when loops cross codimension-2 hinges. FlatInteriorMetric packages the signature, the positivity condition on the Cayley-Menger determinant, and the flatness property. The upstream Simplex3 structure supplies the edge lengths and volume positivity, while the simplicial ledger provides the combinatorial setting. The local theoretical setting is the piecewise-flat manifold model addressing concerns in Regge calculus about interior flatness. This setup ensures that parallel transport inside a single simplex returns the identity, consistent with zero curvature on codimension-0 and codimension-1 cells.
proof idea
The declaration is a pure structure definition that directly declares four fields: the integer signature, the proof that it equals plus or minus one, the Cayley-Menger positivity proposition, and the flat interior proposition. No tactics or lemmas are invoked; the structure serves as an interface for downstream definitions that instantiate it with concrete values such as volume positivity.
why it matters
FlatInteriorMetric provides the foundational data type for equipping simplices with flat interiors, which is consumed by FlatInteriorLedger and InteriorFlatCert. The latter serves as the master certificate that every simplex admits both Euclidean and Minkowski flat interiors, thereby closing the Regge axiom requirement from Beltracchi section 7. In the Recognition Science chain it supports the discrete geometry layer before the continuum bridge is applied, ensuring consistency with the eight-tick octave and spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.