pathWeight_pos
plain-language theorem explainer
The lemma shows that the weight assigned to any recognition path is strictly positive. Modelers of path integrals or amplitudes in the Recognition framework cite it to confirm that weights define valid positive measures. The proof is a one-line term reduction that unfolds the exponential definition of pathWeight and invokes the positivity of the real exponential.
Claim. For every recognition path $γ$, the weight $w[γ] := exp(-C[γ])$ satisfies $0 < w[γ]$.
background
RecognitionPath is a structure with positive duration $T$ and a strictly positive rate function on the interval $[0,T]$. The path weight is defined by pathWeight $γ$ = Real.exp(-pathAction $γ$), where pathAction is the integrated J-cost $C[γ] = ∫ J(r(t)) dt$ along the path. This module supplies a minimal interface for recognition paths, actions, and weights while omitting measure-theoretic lemmas to keep the build surface stable for paper exports. The result depends on the pathWeight definition and the standard fact that the real exponential is positive.
proof idea
The proof is a term-mode one-liner. It unfolds pathWeight to expose Real.exp(-pathAction γ) and then applies Real.exp_pos, the fact that exp(x) > 0 for every real x.
why it matters
This lemma guarantees that weights derived from the J-cost remain positive, which is required for interpreting them as probabilities or for taking square roots to form amplitudes. It supports the sibling construction amplitude_mod_sq_eq_weight. In the Recognition framework it aligns with the exponential map used in path measures and with the positivity built into the forcing chain from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.