def
definition
pathIntegralCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.PathIntegralFromRS on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
38 classical : Jcost 1 = 0
39 quantum : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
40
41def pathIntegralCert : PathIntegralCert where
42 five_formulations := pathIntegralCount
43 classical := classical_path
44 quantum := quantum_fluctuation
45
46end IndisputableMonolith.Physics.PathIntegralFromRS