path_weight
The path weight defines the exponential factor exp(-J(r)/ℏ) that assigns a positive real multiplier to each path labeled by its J-cost r in the Recognition Science path integral. Researchers deriving the partition function or classical limit from the J-action would cite this as the primitive weight. It is introduced by a direct definition that transcribes the standard Feynman form using the J-cost action.
claimThe path weight for J-cost value $r$ and reduced Planck constant $ħ$ is given by $w(r, ħ) = 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 measure concentrating near the classical path because J is convex and its Hessian is calibrated so that J''(1) = 1. Fluctuations are suppressed by the factor exp(-J(γ)/ℏ). The constant ħ appears via the upstream definition ħ = cLagLock · τ₀ = φ^{-5} in RS-native units (Constants.hbar).
proof idea
Direct definition that expands to Real.exp(-(Jcost r)/hbar). No lemmas or tactics are invoked; the body is a single expression that downstream results unfold and rewrite.
why it matters in Recognition Science
This definition supplies the weight appearing in PathIntegralDeepCert (positivity, maximization at r = 1, and unit value at equilibrium) and in the Gaussian approximation theorem. It realizes the structural claim that the path integral measure is exp(-J/ℏ) Dγ, connecting to the J-uniqueness fixed point (T5) and the classical limit ħ → 0. The module states it is part of a zero-sorry structural theorem for the path integral.
scope and limits
- Does not prove positivity or maximization (those are separate theorems).
- Does not restrict the domain of r beyond the reals.
- Does not evaluate the integral or produce a numerical partition function.
- Does not encode any specific discretization of paths.
formal statement (Lean)
36def path_weight (r hbar : ℝ) : ℝ := Real.exp (-(Jcost r) / hbar)
proof body
Definition body.
37
38/-- Path weight is always positive. -/