path_weight
Path weight supplies the exponential factor exp(-J(r)/ℏ) in the J-cost path integral. Derivations of the partition function and classical limit in Recognition Science cite this definition. It is implemented as a direct mapping from the Jcost function and the RS-native hbar value.
claimThe path weight for a configuration with J-cost r is given by $w(r, ħ) = exp(-J(r)/ħ)$, where $J$ is the J-cost function and $ħ$ is the reduced Planck constant in RS-native units.
background
The PathIntegralDeep module constructs the path integral from the J-cost action S[γ] = ∫ J(γ(t)) dt. Fluctuations around the classical path decay as exp(-J(γ)/ℏ) because J is convex with Hessian calibrated at J''(1) = 1. The constant hbar is supplied by Constants.hbar as φ^{-5} in RS units, consistent with the forcing chain T5-T8.
proof idea
This is a one-line definition that applies the real exponential function to the negated ratio of Jcost r and hbar. No lemmas or tactics are invoked beyond the standard Real.exp constructor.
why it matters in Recognition Science
The definition underpins PathIntegralDeepCert and the theorems gaussian_approx_at_eq and path_weight_max_at_eq. It completes the structural theorem for the path integral derived from J-action in the Recognition Science framework. The construction relies on J-convexity and supports concentration on classical paths in the ħ → 0 limit.
scope and limits
- Does not prove positivity of the weight for arbitrary r and hbar.
- Does not establish the maximum value at r = 1.
- Does not derive the Gaussian approximation near equilibrium.
- Does not specify the path measure or integration domain.
formal statement (Lean)
36def path_weight (r hbar : ℝ) : ℝ := Real.exp (-(Jcost r) / hbar)
proof body
Definition body.
37
38/-- Path weight is always positive. -/