pathWeight_pos
The lemma establishes that the weight assigned to any recognition path is strictly positive. Researchers modeling quantum amplitudes via recognition paths would cite it to guarantee that weights remain positive for normalization. The proof is a one-line wrapper that unfolds the definition of pathWeight and invokes the positivity of the real exponential.
claimFor any recognition path $γ$, the path weight $w[γ] = exp(-C[γ])$ satisfies $0 < w[γ]$.
background
RecognitionPath is a structure consisting of a positive time interval T and a positive rate function on the closed interval [0,T]. pathWeight is defined as the real exponential of the negative path action, yielding the positive weight w[γ]. This module supplies a minimal interface for recognition paths and their weights in the Measurement domain, deliberately omitting measure-theoretic details to maintain build stability for paper exports.
proof idea
The proof is a one-line wrapper. It unfolds the definition of pathWeight to expose Real.exp(-pathAction γ), then applies the standard fact that the real exponential is strictly positive for every real argument.
why it matters in Recognition Science
This lemma guarantees positivity of weights in the path formulation, a prerequisite for interpreting w[γ] as a probability factor or for the amplitude bridge where the squared modulus equals the weight. It supports the sibling amplitude_mod_sq_eq_weight result. In the Recognition framework the positivity follows directly from the exponential form of weights derived from the J-cost and the positive-rate constraint built into RecognitionPath.
scope and limits
- Does not bound the numerical magnitude of the weight.
- Does not extend positivity to objects outside the RecognitionPath structure.
- Does not compute or estimate the value of the underlying action integral.
- Does not address the phase or complex structure of amplitudes.
formal statement (Lean)
37lemma pathWeight_pos (γ : RecognitionPath) : 0 < pathWeight γ := by
proof body
Term-mode proof.
38 unfold pathWeight
39 exact Real.exp_pos _
40
41/-- Amplitude modulus squared equals weight. -/