`IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloserAudit`

IndisputableMonolith/Gravity/Analysis/Regge4DTensorAlgebraicCloserAudit.lean · 20 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser
   2
   3/-!
   4# Audit: 4D tensor algebraic closer (partial)
   5-/
   6
   7open IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser
   8
   9#print axioms distinctHingeMomentForm_smul
  10#print axioms distinctHingeMomentForm_axisTTPlus_symbolDir
  11#print axioms distinctHingeMomentForm_axisTTCross_symbolDir
  12#print axioms distinctHingeMomentForm_axisTTPlus_e0Dir
  13#print axioms distinctHingeMomentForm_axisTTCross_e0Dir
  14#print axioms continuumFace_normalizedPlus_symbolDir
  15#print axioms continuumFace_normalizedCross_e0Dir
  16#print axioms continuumFace_normalizedPlus_e0Dir_vanishes
  17#print axioms residual_factor_four_arithmetic
  18#print axioms axis_isotropy_blocker_negated
  19#print axioms does_not_flip_gap_action_recovery
  20

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