module module

`IndisputableMonolith.Foundation.SimplicialLedger.InteriorFlat`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.SimplicialLedger module_import
IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge module_import

declarations in this module (16)

structure FlatInteriorMetric L94
def defaultEuclideanInterior L111
def defaultMinkowskiInterior L121
def InteriorLoop L137
theorem trivial_interior_loop L141
theorem interior_holonomy_trivial L154
structure Hinge L163
inductive NonHingeStratum L169
def deficitOnNonHinge L175
theorem curvature_only_on_hinges L179
structure FlatInteriorLedger L188
def canonicalEuclideanEnrichment L194
def canonicalMinkowskiEnrichment L202
theorem interior_jcost_const_consistent L214
structure InteriorFlatCert L228
def interiorFlatCert L241