module module

`IndisputableMonolith.Gravity.ClausiusEinsteinBridge`

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

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

IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4D module_import
IndisputableMonolith.Gravity.NullConeQuadraticTensorClass module_import
IndisputableMonolith.Gravity.RecordFluxStress module_import
IndisputableMonolith.Gravity.RSNullFieldEquation module_import
IndisputableMonolith.Relativity.Geometry.LocalAreaRaychaudhuri module_import

declarations in this module (16)

def Symmetric4 L23
def minkowskiEta4 L27
def quadContr L31
def MinkowskiNull L35
def vec4 L39
lemma vec4_zero L42
lemma vec4_one L45
lemma vec4_two L48
lemma vec4_three L51
lemma sum_fin_four L54
theorem quadContr_minkowskiEta4 L62
theorem pointwise_eq_implies_null_cut_eq L70
theorem null_cut_eq_not_pointwise_eq L80
theorem null_quadratic_zero_eq_scalar_eta L108
theorem null_quadratic_eq_of_diff_scalar_eta L158
theorem einstein_equation_shaped_of_local_clausius L191