module module

`IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence`

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 (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge module_import
IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge module_import
IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi module_import

declarations in this module (11)

def HingeTrivial L88
theorem trivial_hinge_contribution L93
theorem regge_sum_append_trivial L102
theorem regge_sum_append L131
theorem regge_sum_nil L140
structure SimplicialRefinement L157
theorem regge_sum_refinement_invariant L173
theorem refinement_discharge_inherits L191
theorem refinement_calibrated L210
structure CubicSimplicialInvarianceCert L233
theorem cubicSimplicialInvarianceCert L259