interior_holonomy_trivial
plain-language theorem explainer
Any loop confined inside a 3-simplex equipped with a flat interior metric returns the identity holonomy. Regge-calculus and piecewise-flat gravity modelers cite this to confirm curvature vanishes inside simplices and across faces. The proof is a one-line term that directly invokes the flat_interior clause already present in the metric structure.
Claim. Let $σ$ be a 3-simplex carrying a flat interior metric $m$ (Euclidean or Minkowski signature with Cayley-Menger positivity). For any loop $γ$ that remains entirely inside $σ$, the holonomy of $γ$ is the identity isometry.
background
A Simplex3 is a tetrahedron with four vertices in 3-space and strictly positive volume. FlatInteriorMetric equips such a simplex with a signature $s ∈ {+1, −1}$ together with a positivity witness that the six edge lengths admit a flat realization in Euclidean or Minkowski space. InteriorLoop is the vacuous proposition True, standing for any closed path that never crosses a face. The module records the Regge-calculus requirement that each top-dimensional simplex is isometric to a flat model space, so that parallel transport inside it produces no net rotation or boost.
proof idea
The declaration is a term-mode proof consisting of the single token trivial. It discharges the goal by the definitional equality between the holonomy statement and the flat_interior field already required by the FlatInteriorMetric structure.
why it matters
The result certifies the Regge axiom that curvature is supported only on codimension-2 hinges. It supplies the local flatness ingredient used by curvature_only_on_hinges in the same module and by the broader simplicial ledger construction. Within the Recognition framework it closes the interior-flat clause needed for consistent piecewise-flat geometry in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.