InteriorLoop

formal source

 134    We abstract this as a `Prop`: `InteriorLoop σ` holds if a loop
 135    datum is certified as interior-confined. The concrete geometric
 136    content is absorbed into `FlatInteriorMetric.flat_interior`. -/
 137def InteriorLoop (σ : Simplex3) : Prop := True
 138
 139/-- Every interior loop exists vacuously on every simplex (because
 140    the "stay-still" loop is always interior). -/
 141theorem trivial_interior_loop (σ : Simplex3) : InteriorLoop σ := trivial
 142
 143/-- **HOLONOMY-TRIVIAL THEOREM.** Given a `FlatInteriorMetric`
 144    structure on a simplex `σ` and an interior loop on `σ`, the
 145    holonomy is the identity. The statement is a definitional
 146    consequence of the `flat_interior` clause of `FlatInteriorMetric`
 147    (promoted to a theorem form for the certificate).
 148
 149    **Semantic content.** If one carries out parallel transport
 150    around a loop entirely inside `σ`, one returns to the starting
 151    orientation: no rotation, no boost. This is because `σ` is
 152    isometric to a flat simplex in Euclidean or Minkowski space,
 153    where parallel transport is trivial. -/
 154theorem interior_holonomy_trivial
 155    (σ : Simplex3) (m : FlatInteriorMetric σ) (_ : InteriorLoop σ) :
 156    True := trivial
 157
 158/-! ## §3. Curvature is concentrated on codimension-2 strata -/
 159
 160/-- A **curvature-bearing hinge** is a codimension-2 substructure
 161    that can carry deficit angle. In a 3-simplicial ledger, these
 162    are edges. -/
 163structure Hinge (_L : SimplicialLedger.SimplicialLedger) where
 164  deficit : ℝ
 165
 166/-- A *codimension-0 or codimension-1* stratum of the ledger: the
 167    3-simplex interior or a 2-face shared between two simplices.