`IndisputableMonolith.Gravity.RSNullFieldEquationAudit`

IndisputableMonolith/Gravity/RSNullFieldEquationAudit.lean · 18 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.RSNullFieldEquation
   2
   3/-!
   4Axiom audit for the matrix-level RS null-field reduction.
   5-/
   6
   7open IndisputableMonolith.Gravity.RSNullFieldReduction
   8
   9#print axioms quadContr_add
  10#print axioms quadContr_smul
  11#print axioms quadContr_metric_term_eq_zero
  12#print axioms null_scalar_of_einstein_shaped
  13#print axioms null_scalar_of_source
  14#print axioms rs_null_scalar_of_source
  15#print axioms source_of_componentwise
  16#print axioms scalar_metric_term_is_null_invisible
  17#print axioms rsNullFieldReductionCert
  18

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