module module

`IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi`

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

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem module_import
IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge module_import
IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence module_import
IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge module_import
IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge module_import
IndisputableMonolith.Gravity.WeakFieldConformalRegge module_import

depends on (4)

Lean names referenced from this declaration's body.

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

declarations in this module (18)

theorem is L36
abbrev LogPotential L70
structure EdgeLengthField L76
def conformal_edge_length_field L90
theorem conformal_edge_length_flat L106
structure HingeDatum L127
structure DeficitAngleFunctional L136
def regge_sum L143
def ReggeDeficitLinearizationHypothesis L178
theorem field_curvature_identity_under_linearization L194
theorem laplacian_action_flat L231
theorem regge_sum_flat_under_linearization L239
def logPotentialOf L254
theorem logPotentialOf_flat L258
theorem jcost_to_regge_factor_eq_kappa_einstein L279
theorem kappa_calibration_positive L290
structure EdgeLengthFromPsiCert L301
theorem edgeLengthFromPsiCert L320