`IndisputableMonolith.Gravity.NullConeQuadraticTensorClassAudit`

IndisputableMonolith/Gravity/NullConeQuadraticTensorClassAudit.lean · 29 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.NullConeQuadraticTensorClass
   2
   3/-!
   4Axiom audit for the Phase-5 algebraic null-cone rigidity prerequisite.
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Gravity
   9namespace NullConeQuadraticTensorClass
  10
  11#print axioms symmetrize4_symmetric
  12#print axioms quadContr_eq_quadContr_symmetrize4
  13#print axioms quadContr_antisymmetrize4_eq_zero
  14#print axioms quadContr_neg
  15#print axioms all_null_quad_eq_of_future_nonzero_null_quad_eq
  16#print axioms null_quadratic_eq_implies_diff_scalar_eta
  17#print axioms future_null_quadratic_eq_implies_diff_scalar_eta
  18#print axioms diff_scalar_eta_implies_null_quadratic_eq
  19#print axioms null_quadratic_eq_iff_diff_scalar_eta
  20#print axioms null_quadratic_eq_iff_symmetrize_diff_scalar_eta
  21#print axioms determinesAlgebraicNullQuadraticClass_quadContr
  22#print axioms fixedSymmetricStress_determinesAlgebraicNullQuadraticClass
  23#print axioms fixedSymmetricStress_null_class_unique
  24#print axioms nullConeQuadraticTensorClassCert
  25
  26end NullConeQuadraticTensorClass
  27end Gravity
  28end IndisputableMonolith
  29

source mirrored from github.com/jonwashburn/shape-of-logic