`IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4DAudit`

IndisputableMonolith/Gravity/Analysis/ReggeExactFlatHessianSymbol4DAudit.lean · 21 lines · 1 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D
   2open IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D
   3#print axioms ExactHessianTTIsotropyTarget_closed
   4#print axioms ExactHessianGaugeZeroTarget_algebraic_face
   5#print axioms ExactHessianS_RS_converges_EH_4d_closed
   6#print axioms ExactHessianEdgeOriginsM2Banked_closed
   7#print axioms exact_hessian_algebraic_face_banked
   8#print axioms exact_hessian_srs_still_open
   9theorem exact_hessian_audit_package :
  10    ExactHessianTTIsotropyTarget ∧
  11      ExactHessianGaugeZeroTarget ∧
  12        ExactHessianEdgeOriginsM2Banked ∧
  13          ExactHessianNormalizationGatePass = true ∧
  14            ExactHessianAlgebraicM2TablePresent = false ∧
  15              exactHessianSymbolStatus.srsInhabited = false ∧
  16                exactHessianSymbolStatus.gapActionRecovery = false :=
  17  ⟨ExactHessianTTIsotropyTarget_closed, ExactHessianGaugeZeroTarget_algebraic_face,
  18    ExactHessianEdgeOriginsM2Banked_closed, exactHessianNormalizationGatePass_true,
  19    rfl, rfl, rfl⟩
  20#print axioms exact_hessian_audit_package
  21

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