path_weight_pos
The declaration establishes that the path weight exp(-J(r)/ℏ) is strictly positive for every real r and ℏ. Researchers constructing the path integral measure from the J-cost action in Recognition Science cite it to ensure the partition function and probability weights remain well-defined and positive. The proof is a one-line term reduction to the positivity of the real exponential.
claimFor all real numbers $r$ and $ħ$, $0 < exp(-J(r)/ħ)$, where $J$ is the J-cost function.
background
The module derives the Feynman path integral from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, with the path weight defined as exp(-J(r)/ℏ). Here ℏ is the RS-native reduced Planck constant φ^{-5}. The local setting is the structural theorem establishing that the measure concentrates near the classical path because J is convex with Hessian calibrated to J''(1) = 1, so fluctuations decay as exp(-J(γ)/ℏ).
proof idea
The proof is a one-line term wrapper that applies Real.exp_pos directly to the definition of path_weight, which is constructed as Real.exp (-(Jcost r) / hbar).
why it matters in Recognition Science
This theorem supplies the path_weight_pos field of the PathIntegralDeepCert structure, which also records maximization at r = 1 and unit weight at equilibrium. It is invoked in Modal.Actualization to obtain the Born rule P[γ] = W[γ] / Σ W[γ']. In the framework it supports the classical limit ℏ → 0 and the Gaussian approximation near the minimum action J(1) = 0, consistent with the RCL and the eight-tick octave.
scope and limits
- Does not establish positivity when ℏ ≤ 0.
- Does not address convergence of the integral over all paths.
- Does not extend to complex-valued weights or phases.
- Does not derive the result from the forcing chain T5-T8.
Lean usage
path_weight_pos r hbarformal statement (Lean)
39theorem path_weight_pos (r hbar : ℝ) : 0 < path_weight r hbar :=
proof body
Term-mode proof.
40 Real.exp_pos _
41
42/-- Path weight is maximized at r = 1 (minimum action = 0). -/