`IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4DAudit`

IndisputableMonolith/Gravity/Analysis/ReggeExactFlatHessianBlochSymbol4DAudit.lean · 17 lines · 1 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
   3open IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   4open IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D
   5open IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
   6#print axioms tendsto_exactMidpointBloch_centered_div_sq
   7#print axioms tendsto_exactMidpointBloch_m2_div
   8#print axioms gate_passes_with_discrete_bookkeeping
   9theorem bloch_symbol_audit_package :
  10    couplingTable.size = 1208 ∧
  11      exactBlochSymbolStatus.specializedTendstoProved = true ∧
  12        exactBlochSymbolStatus.srsInhabited = false ∧
  13          exactBlochSymbolStatus.gapActionRecovery = false ∧
  14            NormalizationGatePass = true :=
  15  ⟨couplingTable_size, rfl, rfl, rfl, normalizationGatePass_true⟩
  16#print axioms bloch_symbol_audit_package
  17

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