IndisputableMonolith.Gravity.DiscreteVacuumEinstein

declarations in this module (17)

• def ZeroDeficitAtFlat L28
• def CriticalAtFlat L32
• def vertexEdgeIncidenceDerivative L38
• def directionalLengthCoefficient L44
• def HingeDerivativeMatchesIncidence L52
• theorem hingeDerivative_matches_incidence_simplified L59
• def IncidenceDeficitSeparating L72
• def IncidenceDeficitRecovering L80
• theorem incidenceDeficitSeparating_of_recovering L90
• structure RecoveringIncidenceTriangulation L105
• structure ReggeFirstVariationFormula L115
• theorem zero_deficit_of_flat_configuration L145
• structure DiscreteVacuumEinsteinInput L154
• theorem reggeAction_critical_iff_zero_deficit L161
• theorem zero_deficit_of_critical_of_variationFormula_of_separating L168
• def discreteVacuumEinsteinInput_of_variationFormula_of_separating L193
• def discreteVacuumEinsteinInput_of_recoveringIncidence L208