Hinge

formal source

 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.
 168    Neither carries curvature by the flat-interior axiom. -/
 169inductive NonHingeStratum (L : SimplicialLedger.SimplicialLedger) : Type
 170  | interior (σ : Simplex3) : NonHingeStratum L
 171  | face (σ₁ σ₂ : Simplex3) : NonHingeStratum L
 172
 173/-- The deficit on a non-hinge stratum is zero. This encodes the
 174    physical axiom that curvature is only at codimension-2. -/
 175def deficitOnNonHinge {L : SimplicialLedger.SimplicialLedger}
 176    (_s : NonHingeStratum L) : ℝ := 0
 177
 178/-- Zero-deficit on non-hinge strata is a definitional theorem. -/
 179theorem curvature_only_on_hinges {L : SimplicialLedger.SimplicialLedger}
 180    (s : NonHingeStratum L) : deficitOnNonHinge s = 0 := rfl
 181
 182/-! ## §4. Flat-interior ledger and the enriched structure -/
 183
 184/-- A **flat-interior ledger** is a simplicial ledger in which every
 185    simplex is equipped with a flat-interior metric structure.
 186    This is the Lean formalization of Philip's "ledger cells
 187    filled with flat space". -/
 188structure FlatInteriorLedger where
 189  base : SimplicialLedger.SimplicialLedger
 190  metric : ∀ σ ∈ base.simplices, FlatInteriorMetric σ
 191
 192/-- The **canonical Euclidean enrichment** of any simplicial ledger.
 193    Every simplex is assigned the default Euclidean interior. -/