`IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBindingAudit`

IndisputableMonolith/Gravity/SevenGaps/DiracAlgebraContinuumBindingAudit.lean · 25 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBinding
   2
   3/-!
   4# Axiom audit: Wave C2 R4 repaired Dirac algebra continuum limit
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBinding
  11
  12#check sampledPhasePoint
  13#check sampledLapse
  14#check periodicSampledDynamicBracketSum
  15#check continuumLatticeBracket
  16#check bracket_HamDynN_eq_periodicSampled
  17#check periodicSampled_eq_sampled_of_periodic
  18#check dirac_algebra_continuum_limit
  19#check dirac_algebra_continuum_limit_hamDynN
  20
  21#print axioms bracket_HamDynN_eq_periodicSampled
  22#print axioms periodicSampled_eq_sampled_of_periodic
  23#print axioms dirac_algebra_continuum_limit
  24#print axioms dirac_algebra_continuum_limit_hamDynN
  25

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