trivial_interior_loop
plain-language theorem explainer
Every 3-simplex admits an interior loop because the definition of InteriorLoop reduces to the proposition True. Regge-calculus and piecewise-flat manifold workers cite this when confirming that paths confined to a simplex interior accrue zero holonomy. The proof is a one-line term that supplies the trivial inhabitant of True.
Claim. For every 3-simplex $σ$, the proposition InteriorLoop($σ$) holds, where InteriorLoop($σ$) is the vacuous claim that a closed cycle of micro-steps remains inside $σ$ (the stay-still loop satisfies the condition).
background
The module establishes that each 3-simplex carries a flat interior metric isometric to Euclidean or Minkowski space, with curvature confined to codimension-2 hinges. InteriorLoop($σ$) is defined as the proposition True, absorbing the geometric content that any loop staying inside $σ$ never crosses a hinge. The module doc states: “A loop γ that does not cross any hinge returns a holonomy of 1 in the isometry group of the flat interior.”
proof idea
The proof is a one-line term that applies the trivial inhabitant of the proposition True, which is the body of the definition of InteriorLoop.
why it matters
This supplies the base case for the holonomy-trivial property inside flat simplices, directly implementing the Regge axiom that curvature concentrates on codimension-2 hinges. It fills the explicit flat-interior structure required to address Beltracchi §7. The declaration sits at the root of the module’s three listed results on interior-flat simplices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.