classical_path

formal source

  27theorem pathIntegralCount : Fintype.card PathIntegralFormulation = 5 := by decide
  28
  29/-- Classical path: J = 0 (Euler-Lagrange stationary point). -/
  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