  30theorem classical_path : Jcost 1 = 0 := Jcost_unit0
  31
  32/-- Quantum fluctuations: J > 0 (off-classical paths). -/
  33theorem quantum_fluctuation {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  34    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  35
  36structure PathIntegralCert where
  37  five_formulations : Fintype.card PathIntegralFormulation = 5
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.