IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser

declarations in this module (21)

• abbrev Mat4 L53
• def distinctHingeMomentForm L60
• theorem distinctHingeMomentForm_smul L63
• theorem distinctHingeMomentForm_zero L68
• theorem distinctHingeMomentForm_axisTTPlus_symbolDir L74
• theorem distinctHingeMomentForm_axisTTCross_symbolDir L78
• theorem distinctHingeMomentForm_axisTTPlus_e0Dir L82
• theorem distinctHingeMomentForm_axisTTCross_e0Dir L86
• theorem continuumFace_normalizedPlus_symbolDir L92
• theorem continuumFace_normalizedCross_e0Dir L103
• theorem continuumFace_normalizedPlus_e0Dir_vanishes L112
• def Regge4DDistinctHingeTensorClosedFormOpen L126
• theorem residual_factor_four_arithmetic L136
• theorem inhabits L145
• def Regge4DDistinctHingePinnedVsEHFactor4 L147
• theorem Regge4DDistinctHingePinnedVsEHFactor4_status_open L151
• theorem axis_isotropy_blocker_negated L155
• structure Regge4DTensorAlgebraicCloserStatus L159
• def regge4DTensorAlgebraicCloserStatus L167
• theorem regge4DTensorAlgebraicCloserStatus_flags L175
• theorem does_not_flip_gap_action_recovery L185