`IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DAudit`

IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DAudit.lean · 27 lines · 1 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
   2
   3open IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
   4open IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D.KernelCert
   5
   6/-!
   7Audit for typed blocker `exact_midpoint_m2_tt_identity` (kernel upgrade).
   8
   9Expected axiom set for the main identity and table certificates:
  10`[propext, Classical.choice, Quot.sound]` — no `Lean.ofReduceBool` /
  11`Lean.trustCompiler`.
  12-/
  13
  14#print axioms m2Coeff_eq_explicitM2Coeff
  15#print axioms symFull_explicit_eq_symFull_closed
  16#print axioms exactMidpointBlochM2_eq_biquad
  17#print axioms biquad_symFull
  18#print axioms biquad_closedCoeff_eq_closedForm
  19#print axioms exactMidpointBlochM2_eq_closedForm_of_symmetric
  20#print axioms exactMidpointBlochM2_eq_neg_eighth_frobenius_tt
  21
  22theorem m2_tt_identity_audit_package :
  23    ExactMidpointM2TTIdentityProved = true :=
  24  exactMidpointM2TTIdentityProved_true
  25
  26#print axioms m2_tt_identity_audit_package
  27

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