path_weight_pos
plain-language theorem explainer
The path weight exp(-J(r)/ℏ) is strictly positive for all real r and ħ. Researchers deriving the partition function or Born rule from the J-cost action would cite this when confirming the measure is well-defined. The proof is a one-line term application of Real.exp_pos to the definition of path_weight.
Claim. For all real numbers $r$ and $ħ$, one has $0 < exp(-J(r)/ħ)$, where $J$ is the J-cost function and $ħ$ is the reduced Planck constant.
background
The module establishes the Feynman path integral from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, with the weight function defined as exp(-J(r)/ħ). The constant ħ is supplied by Constants.hbar as φ^{-5} in RS-native units. The sibling definition path_weight supplies the explicit form exp(-(Jcost r)/hbar), and upstream results include the hbar definitions from Constants and Codata together with the J-cost primitives.
proof idea
The proof is a one-line term that applies Real.exp_pos directly to the argument of the exponential appearing in the definition of path_weight.
why it matters
This theorem supplies the first field of the PathIntegralDeepCert structure and is reused in the Modal.Actualization and ModalGeometry modules. It completes one of the four structural properties listed in the module doc-comment for the J-cost derivation of the path integral, aligning with the convexity and minimum of J at 1 from the T5 J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.