module
module
IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge
show as:
view Lean formalization →
depends on (8)
-
IndisputableMonolith.Constants -
IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge -
IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge -
IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi -
IndisputableMonolith.Geometry.CayleyMenger -
IndisputableMonolith.Geometry.DeficitLinearization -
IndisputableMonolith.Geometry.DihedralAngle -
IndisputableMonolith.Geometry.Schlaefli
declarations in this module (8)
-
def
CalibratedAgainstGraph -
theorem
calibrated_iff_hypothesis -
theorem
simplicial_linearization_discharge -
theorem
cubic_calibrated_against_graph -
theorem
field_curvature_identity_simplicial -
theorem
field_curvature_identity_simplicial_einstein -
structure
SimplicialFieldCurvatureCert -
theorem
simplicialFieldCurvatureCert