InteriorLoop
plain-language theorem explainer
InteriorLoop σ is the predicate asserting that a closed cycle of micro-steps on a 3-simplex σ remains confined to its interior without crossing any hinge. Regge-calculus and discrete-gravity researchers cite it when localizing curvature exclusively to codimension-2 strata. The declaration is a one-line definition that sets the predicate identically to True, encoding the vacuous stay-still loop.
Claim. For any 3-simplex $σ$, the predicate InteriorLoop($σ$) holds if and only if every closed cycle of micro-steps on $σ$ stays inside the interior of $σ$ (never crossing a hinge).
background
A Simplex3 is the basic volume element of the simplicial ledger: a tetrahedron whose four vertices lie in $ℝ^3$ and whose volume is strictly positive. FlatInteriorMetric on $σ$ records a signature choice ($+1$ Euclidean or $-1$ Minkowski) together with a Cayley-Menger positivity witness that the edge lengths realize a flat interior metric. The module InteriorFlat makes explicit the Regge-calculus fact that each top-dimensional simplex carries a flat metric while curvature is supported only on codimension-2 hinges.
proof idea
The declaration is a one-line definition that sets InteriorLoop σ to the constant proposition True. This directly implements the comment that the stay-still loop is always interior, supplying the vacuous truth required by downstream statements such as trivial_interior_loop and interior_holonomy_trivial.
why it matters
InteriorLoop supplies the hypothesis used by interior_holonomy_trivial, which asserts that parallel transport around any interior loop returns the identity isometry. It thereby closes the formal gap noted in the module documentation for Beltracchi §7: the simplicial ledger now records that no curvature accrues inside a simplex or across a face. The definition aligns with the Recognition Science concentration of curvature on hinges and with the eight-tick octave structure in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.